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

Metamath Proof Explorer

Theorem lemul1

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

Ref Expression
Assertion lemul1 
|- ( ( 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 ltmul1 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A x. C ) < ( B x. C ) ) )
2 recn 
 |-  ( A e. RR -> A e. CC )
3 recn 
 |-  ( B e. RR -> B e. CC )
4 recn 
 |-  ( C e. RR -> C e. CC )
5 4 adantr 
 |-  ( ( C e. RR /\ 0 < C ) -> C e. CC )
6 gt0ne0 
 |-  ( ( C e. RR /\ 0 < C ) -> C =/= 0 )
7 5 6 jca 
 |-  ( ( C e. RR /\ 0 < C ) -> ( C e. CC /\ C =/= 0 ) )
8 mulcan2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )
9 2 3 7 8 syl3an 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )
10 9 bicomd 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A = B <-> ( A x. C ) = ( B x. C ) ) )
11 1 10 orbi12d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A < B \/ A = B ) <-> ( ( A x. C ) < ( B x. C ) \/ ( A x. C ) = ( B x. C ) ) ) )
12 leloe 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
13 12 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
14 remulcl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
15 14 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
16 remulcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B x. C ) e. RR )
17 16 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B x. C ) e. RR )
18 15 17 leloed 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <_ ( B x. C ) <-> ( ( A x. C ) < ( B x. C ) \/ ( A x. C ) = ( B x. C ) ) ) )
19 18 3adant3r 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) <_ ( B x. C ) <-> ( ( A x. C ) < ( B x. C ) \/ ( A x. C ) = ( B x. C ) ) ) )
20 11 13 19 3bitr4d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( A x. C ) <_ ( B x. C ) ) )