Metamath Proof Explorer

Theorem ltmul1

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) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion ltmul1 
|- ( ( 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 ltmul1a 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> ( A x. C ) < ( B x. C ) )
2 1 ex 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B -> ( A x. C ) < ( B x. C ) ) )
3 oveq1 
 |-  ( A = B -> ( A x. C ) = ( B x. C ) )
4 3 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A = B -> ( A x. C ) = ( B x. C ) ) )
5 ltmul1a 
 |-  ( ( ( B e. RR /\ A e. RR /\ ( C e. RR /\ 0 < C ) ) /\ B < A ) -> ( B x. C ) < ( A x. C ) )
6 5 ex 
 |-  ( ( B e. RR /\ A e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B < A -> ( B x. C ) < ( A x. C ) ) )
7 6 3com12 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B < A -> ( B x. C ) < ( A x. C ) ) )
8 4 7 orim12d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A = B \/ B < A ) -> ( ( A x. C ) = ( B x. C ) \/ ( B x. C ) < ( A x. C ) ) ) )
9 8 con3d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( -. ( ( A x. C ) = ( B x. C ) \/ ( B x. C ) < ( A x. C ) ) -> -. ( A = B \/ B < A ) ) )
10 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> A e. RR )
11 simp3l 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C e. RR )
12 10 11 remulcld 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A x. C ) e. RR )
13 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> B e. RR )
14 13 11 remulcld 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B x. C ) e. RR )
15 12 14 lttrid 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < ( B x. C ) <-> -. ( ( A x. C ) = ( B x. C ) \/ ( B x. C ) < ( A x. C ) ) ) )
16 10 13 lttrid 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
17 9 15 16 3imtr4d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < ( B x. C ) -> A < B ) )
18 2 17 impbid 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A x. C ) < ( B x. C ) ) )