MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lemul1a Structured version   Unicode version

Theorem lemul1a 10173
Description: Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by NM, 21-Feb-2005.)
Assertion
Ref Expression
lemul1a  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  ( C  e.  RR  /\  0  <_  C )
)  /\  A  <_  B )  ->  ( A  x.  C )  <_  ( B  x.  C )
)

Proof of Theorem lemul1a
StepHypRef Expression
1 0re 9376 . . . . . . 7  |-  0  e.  RR
2 leloe 9451 . . . . . . 7  |-  ( ( 0  e.  RR  /\  C  e.  RR )  ->  ( 0  <_  C  <->  ( 0  <  C  \/  0  =  C )
) )
31, 2mpan 665 . . . . . 6  |-  ( C  e.  RR  ->  (
0  <_  C  <->  ( 0  <  C  \/  0  =  C ) ) )
43pm5.32i 632 . . . . 5  |-  ( ( C  e.  RR  /\  0  <_  C )  <->  ( C  e.  RR  /\  ( 0  <  C  \/  0  =  C ) ) )
5 lemul1 10171 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  ( C  e.  RR  /\  0  <  C ) )  -> 
( A  <_  B  <->  ( A  x.  C )  <_  ( B  x.  C ) ) )
65biimpd 207 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  ( C  e.  RR  /\  0  <  C ) )  -> 
( A  <_  B  ->  ( A  x.  C
)  <_  ( B  x.  C ) ) )
763expia 1184 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( C  e.  RR  /\  0  < 
C )  ->  ( A  <_  B  ->  ( A  x.  C )  <_  ( B  x.  C
) ) ) )
87com12 31 . . . . . 6  |-  ( ( C  e.  RR  /\  0  <  C )  -> 
( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  ->  ( A  x.  C )  <_  ( B  x.  C
) ) ) )
91leidi 9864 . . . . . . . . . 10  |-  0  <_  0
10 recn 9362 . . . . . . . . . . . 12  |-  ( A  e.  RR  ->  A  e.  CC )
1110mul01d 9558 . . . . . . . . . . 11  |-  ( A  e.  RR  ->  ( A  x.  0 )  =  0 )
12 recn 9362 . . . . . . . . . . . 12  |-  ( B  e.  RR  ->  B  e.  CC )
1312mul01d 9558 . . . . . . . . . . 11  |-  ( B  e.  RR  ->  ( B  x.  0 )  =  0 )
1411, 13breqan12d 4297 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  x.  0 )  <_  ( B  x.  0 )  <->  0  <_  0 ) )
159, 14mpbiri 233 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  0 )  <_  ( B  x.  0 ) )
16 oveq2 6090 . . . . . . . . . 10  |-  ( 0  =  C  ->  ( A  x.  0 )  =  ( A  x.  C ) )
17 oveq2 6090 . . . . . . . . . 10  |-  ( 0  =  C  ->  ( B  x.  0 )  =  ( B  x.  C ) )
1816, 17breq12d 4295 . . . . . . . . 9  |-  ( 0  =  C  ->  (
( A  x.  0 )  <_  ( B  x.  0 )  <->  ( A  x.  C )  <_  ( B  x.  C )
) )
1915, 18syl5ib 219 . . . . . . . 8  |-  ( 0  =  C  ->  (
( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  C )  <_  ( B  x.  C )
) )
2019a1dd 46 . . . . . . 7  |-  ( 0  =  C  ->  (
( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  ->  ( A  x.  C )  <_  ( B  x.  C )
) ) )
2120adantl 463 . . . . . 6  |-  ( ( C  e.  RR  /\  0  =  C )  ->  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  ->  ( A  x.  C )  <_  ( B  x.  C
) ) ) )
228, 21jaodan 778 . . . . 5  |-  ( ( C  e.  RR  /\  ( 0  <  C  \/  0  =  C
) )  ->  (
( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  ->  ( A  x.  C )  <_  ( B  x.  C )
) ) )
234, 22sylbi 195 . . . 4  |-  ( ( C  e.  RR  /\  0  <_  C )  -> 
( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  ->  ( A  x.  C )  <_  ( B  x.  C
) ) ) )
2423com12 31 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( C  e.  RR  /\  0  <_  C )  ->  ( A  <_  B  ->  ( A  x.  C )  <_  ( B  x.  C
) ) ) )
25243impia 1179 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  ( C  e.  RR  /\  0  <_  C ) )  -> 
( A  <_  B  ->  ( A  x.  C
)  <_  ( B  x.  C ) ) )
2625imp 429 1  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  ( C  e.  RR  /\  0  <_  C )
)  /\  A  <_  B )  ->  ( A  x.  C )  <_  ( B  x.  C )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1757   class class class wbr 4282  (class class class)co 6082   RRcr 9271   0cc0 9272    x. cmul 9277    < clt 9408    <_ cle 9409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-op 3874  df-uni 4082  df-br 4283  df-opab 4341  df-mpt 4342  df-id 4625  df-po 4630  df-so 4631  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588
This theorem is referenced by:  lemul2a  10174  ltmul12a  10175  lemul12b  10176  lt2msq1  10205  lemul1ad  10262  faclbnd4lem1  12055  facavg  12063  mulcn2  13059  o1fsum  13261  eftlub  13378  bddmulibl  21160  cxpaddlelem  22076  dchrmusum2  22630  axcontlem7  23041  nmoub3i  23998  siilem1  24076  ubthlem3  24098  bcs2  24409  cnlnadjlem2  25297  leopnmid  25367  eulerpartlemgc  26595  rrntotbnd  28581  jm2.17a  29150
  Copyright terms: Public domain W3C validator