Metamath Proof Explorer

Theorem lt2mul2div

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006)

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

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( C e. RR -> C e. CC )
2 recn 
 |-  ( D e. RR -> D e. CC )
3 mulcom 
 |-  ( ( C e. CC /\ D e. CC ) -> ( C x. D ) = ( D x. C ) )
4 1 2 3 syl2an 
 |-  ( ( C e. RR /\ D e. RR ) -> ( C x. D ) = ( D x. C ) )
5 4 oveq1d 
 |-  ( ( C e. RR /\ D e. RR ) -> ( ( C x. D ) / B ) = ( ( D x. C ) / B ) )
6 5 adantl 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( C x. D ) / B ) = ( ( D x. C ) / B ) )
7 2 ad2antll 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ D e. RR ) ) -> D e. CC )
8 1 ad2antrl 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ D e. RR ) ) -> C e. CC )
9 recn 
 |-  ( B e. RR -> B e. CC )
10 9 adantr 
 |-  ( ( B e. RR /\ 0 < B ) -> B e. CC )
11 gt0ne0 
 |-  ( ( B e. RR /\ 0 < B ) -> B =/= 0 )
12 10 11 jca 
 |-  ( ( B e. RR /\ 0 < B ) -> ( B e. CC /\ B =/= 0 ) )
13 12 adantr 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ D e. RR ) ) -> ( B e. CC /\ B =/= 0 ) )
14 divass 
 |-  ( ( D e. CC /\ C e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( D x. C ) / B ) = ( D x. ( C / B ) ) )
15 7 8 13 14 syl3anc 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( D x. C ) / B ) = ( D x. ( C / B ) ) )
16 6 15 eqtrd 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( C x. D ) / B ) = ( D x. ( C / B ) ) )
17 16 adantrrr 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( C x. D ) / B ) = ( D x. ( C / B ) ) )
18 17 adantll 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( C x. D ) / B ) = ( D x. ( C / B ) ) )
19 18 breq2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( A < ( ( C x. D ) / B ) <-> A < ( D x. ( C / B ) ) ) )
20 simpll 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> A e. RR )
21 remulcl 
 |-  ( ( C e. RR /\ D e. RR ) -> ( C x. D ) e. RR )
22 21 adantrr 
 |-  ( ( C e. RR /\ ( D e. RR /\ 0 < D ) ) -> ( C x. D ) e. RR )
23 22 adantl 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( C x. D ) e. RR )
24 simplr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( B e. RR /\ 0 < B ) )
25 ltmuldiv 
 |-  ( ( A e. RR /\ ( C x. D ) e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( A x. B ) < ( C x. D ) <-> A < ( ( C x. D ) / B ) ) )
26 20 23 24 25 syl3anc 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A x. B ) < ( C x. D ) <-> A < ( ( C x. D ) / B ) ) )
27 simpl 
 |-  ( ( B e. RR /\ 0 < B ) -> B e. RR )
28 27 11 jca 
 |-  ( ( B e. RR /\ 0 < B ) -> ( B e. RR /\ B =/= 0 ) )
29 redivcl 
 |-  ( ( C e. RR /\ B e. RR /\ B =/= 0 ) -> ( C / B ) e. RR )
30 29 3expb 
 |-  ( ( C e. RR /\ ( B e. RR /\ B =/= 0 ) ) -> ( C / B ) e. RR )
31 28 30 sylan2 
 |-  ( ( C e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( C / B ) e. RR )
32 31 ancoms 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ C e. RR ) -> ( C / B ) e. RR )
33 32 ad2ant2lr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( C / B ) e. RR )
34 simprr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( D e. RR /\ 0 < D ) )
35 ltdivmul 
 |-  ( ( A e. RR /\ ( C / B ) e. RR /\ ( D e. RR /\ 0 < D ) ) -> ( ( A / D ) < ( C / B ) <-> A < ( D x. ( C / B ) ) ) )
36 20 33 34 35 syl3anc 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A / D ) < ( C / B ) <-> A < ( D x. ( C / B ) ) ) )
37 19 26 36 3bitr4d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A x. B ) < ( C x. D ) <-> ( A / D ) < ( C / B ) ) )