This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lemul1a

Description: Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by NM, 21-Feb-2005)

Ref Expression
Assertion lemul1a 
|- ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( A x. C ) <_ ( B x. C ) )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 leloe 
 |-  ( ( 0 e. RR /\ C e. RR ) -> ( 0 <_ C <-> ( 0 < C \/ 0 = C ) ) )
3 1 2 mpan 
 |-  ( C e. RR -> ( 0 <_ C <-> ( 0 < C \/ 0 = C ) ) )
4 3 pm5.32i 
 |-  ( ( C e. RR /\ 0 <_ C ) <-> ( C e. RR /\ ( 0 < C \/ 0 = C ) ) )
5 lemul1 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( A x. C ) <_ ( B x. C ) ) )
6 5 biimpd 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B -> ( A x. C ) <_ ( B x. C ) ) )
7 6 3expia 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( C e. RR /\ 0 < C ) -> ( A <_ B -> ( A x. C ) <_ ( B x. C ) ) ) )
8 7 com12 
 |-  ( ( C e. RR /\ 0 < C ) -> ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> ( A x. C ) <_ ( B x. C ) ) ) )
9 1 leidi 
 |-  0 <_ 0
10 recn 
 |-  ( A e. RR -> A e. CC )
11 10 mul01d 
 |-  ( A e. RR -> ( A x. 0 ) = 0 )
12 recn 
 |-  ( B e. RR -> B e. CC )
13 12 mul01d 
 |-  ( B e. RR -> ( B x. 0 ) = 0 )
14 11 13 breqan12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. 0 ) <_ ( B x. 0 ) <-> 0 <_ 0 ) )
15 9 14 mpbiri 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. 0 ) <_ ( B x. 0 ) )
16 oveq2 
 |-  ( 0 = C -> ( A x. 0 ) = ( A x. C ) )
17 oveq2 
 |-  ( 0 = C -> ( B x. 0 ) = ( B x. C ) )
18 16 17 breq12d 
 |-  ( 0 = C -> ( ( A x. 0 ) <_ ( B x. 0 ) <-> ( A x. C ) <_ ( B x. C ) ) )
19 15 18 imbitrid 
 |-  ( 0 = C -> ( ( A e. RR /\ B e. RR ) -> ( A x. C ) <_ ( B x. C ) ) )
20 19 a1dd 
 |-  ( 0 = C -> ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> ( A x. C ) <_ ( B x. C ) ) ) )
21 20 adantl 
 |-  ( ( C e. RR /\ 0 = C ) -> ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> ( A x. C ) <_ ( B x. C ) ) ) )
22 8 21 jaodan 
 |-  ( ( C e. RR /\ ( 0 < C \/ 0 = C ) ) -> ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> ( A x. C ) <_ ( B x. C ) ) ) )
23 4 22 sylbi 
 |-  ( ( C e. RR /\ 0 <_ C ) -> ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> ( A x. C ) <_ ( B x. C ) ) ) )
24 23 com12 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( C e. RR /\ 0 <_ C ) -> ( A <_ B -> ( A x. C ) <_ ( B x. C ) ) ) )
25 24 3impia 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) -> ( A <_ B -> ( A x. C ) <_ ( B x. C ) ) )
26 25 imp 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( A x. C ) <_ ( B x. C ) )