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

Metamath Proof Explorer

Theorem ltmul1a

Description: Lemma for ltmul1 . Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of Apostol p. 20. (Contributed by NM, 15-May-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion ltmul1a 
|- ( ( ( 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 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> B e. RR )
2 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> A e. RR )
3 1 2 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> ( B - A ) e. RR )
4 simpl3l 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> C e. RR )
5 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> A < B )
6 2 1 posdifd 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> ( A < B <-> 0 < ( B - A ) ) )
7 5 6 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> 0 < ( B - A ) )
8 simpl3r 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> 0 < C )
9 3 4 7 8 mulgt0d 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> 0 < ( ( B - A ) x. C ) )
10 1 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> B e. CC )
11 2 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> A e. CC )
12 4 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> C e. CC )
13 10 11 12 subdird 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> ( ( B - A ) x. C ) = ( ( B x. C ) - ( A x. C ) ) )
14 9 13 breqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> 0 < ( ( B x. C ) - ( A x. C ) ) )
15 2 4 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> ( A x. C ) e. RR )
16 1 4 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> ( B x. C ) e. RR )
17 15 16 posdifd 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> ( ( A x. C ) < ( B x. C ) <-> 0 < ( ( B x. C ) - ( A x. C ) ) ) )
18 14 17 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> ( A x. C ) < ( B x. C ) )