Metamath Proof Explorer

Theorem ltmul2

Description: Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of Apostol p. 20. (Contributed by NM, 13-Feb-2005)

Ref Expression
Assertion ltmul2 
|- ( ( 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 ltmul1 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A x. C ) < ( B x. C ) ) )
2 recn 
 |-  ( C e. RR -> C e. CC )
3 recn 
 |-  ( A e. RR -> A e. CC )
4 mulcom 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
5 3 4 sylan 
 |-  ( ( A e. RR /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
6 5 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. CC ) -> ( 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 8 sylan 
 |-  ( ( B e. RR /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
10 9 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
11 6 10 breq12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. CC ) -> ( ( A x. C ) < ( B x. C ) <-> ( C x. A ) < ( C x. B ) ) )
12 2 11 syl3an3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) < ( B x. C ) <-> ( C x. A ) < ( C x. B ) ) )
13 12 3adant3r 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < ( B x. C ) <-> ( C x. A ) < ( C x. B ) ) )
14 1 13 bitrd 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( C x. A ) < ( C x. B ) ) )