Metamath Proof Explorer

Theorem lemul2

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

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

Proof

Step Hyp Ref Expression
1 lemul1 
 |-  ( ( 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 
 |-  ( C e. RR -> C e. CC )
4 mulcom 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
5 2 3 4 syl2an 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A x. C ) = ( C x. A ) )
6 5 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. C ) = ( C x. A ) )
7 recn 
 |-  ( B e. RR -> B e. CC )
8 mulcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
9 7 3 8 syl2an 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B x. C ) = ( C x. B ) )
10 9 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B x. C ) = ( C x. B ) )
11 6 10 breq12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <_ ( B x. C ) <-> ( C x. A ) <_ ( C x. B ) ) )
12 11 3adant3r 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) <_ ( B x. C ) <-> ( C x. A ) <_ ( C x. B ) ) )
13 1 12 bitrd 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( C x. A ) <_ ( C x. B ) ) )