Metamath Proof Explorer

Theorem ledivdiv

Description: Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( B e. RR /\ 0 < B ) -> B e. RR )
2 gt0ne0 
 |-  ( ( B e. RR /\ 0 < B ) -> B =/= 0 )
3 1 2 jca 
 |-  ( ( B e. RR /\ 0 < B ) -> ( B e. RR /\ B =/= 0 ) )
4 redivcl 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A / B ) e. RR )
5 4 3expb 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) ) -> ( A / B ) e. RR )
6 3 5 sylan2 
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( A / B ) e. RR )
7 6 adantlr 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A / B ) e. RR )
8 divgt0 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A / B ) )
9 7 8 jca 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) e. RR /\ 0 < ( A / B ) ) )
10 simpl 
 |-  ( ( D e. RR /\ 0 < D ) -> D e. RR )
11 gt0ne0 
 |-  ( ( D e. RR /\ 0 < D ) -> D =/= 0 )
12 10 11 jca 
 |-  ( ( D e. RR /\ 0 < D ) -> ( D e. RR /\ D =/= 0 ) )
13 redivcl 
 |-  ( ( C e. RR /\ D e. RR /\ D =/= 0 ) -> ( C / D ) e. RR )
14 13 3expb 
 |-  ( ( C e. RR /\ ( D e. RR /\ D =/= 0 ) ) -> ( C / D ) e. RR )
15 12 14 sylan2 
 |-  ( ( C e. RR /\ ( D e. RR /\ 0 < D ) ) -> ( C / D ) e. RR )
16 15 adantlr 
 |-  ( ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) -> ( C / D ) e. RR )
17 divgt0 
 |-  ( ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) -> 0 < ( C / D ) )
18 16 17 jca 
 |-  ( ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) -> ( ( C / D ) e. RR /\ 0 < ( C / D ) ) )
19 lerec 
 |-  ( ( ( ( A / B ) e. RR /\ 0 < ( A / B ) ) /\ ( ( C / D ) e. RR /\ 0 < ( C / D ) ) ) -> ( ( A / B ) <_ ( C / D ) <-> ( 1 / ( C / D ) ) <_ ( 1 / ( A / B ) ) ) )
20 9 18 19 syl2an 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A / B ) <_ ( C / D ) <-> ( 1 / ( C / D ) ) <_ ( 1 / ( A / B ) ) ) )
21 recn 
 |-  ( C e. RR -> C e. CC )
22 21 adantr 
 |-  ( ( C e. RR /\ 0 < C ) -> C e. CC )
23 gt0ne0 
 |-  ( ( C e. RR /\ 0 < C ) -> C =/= 0 )
24 22 23 jca 
 |-  ( ( C e. RR /\ 0 < C ) -> ( C e. CC /\ C =/= 0 ) )
25 recn 
 |-  ( D e. RR -> D e. CC )
26 25 adantr 
 |-  ( ( D e. RR /\ 0 < D ) -> D e. CC )
27 26 11 jca 
 |-  ( ( D e. RR /\ 0 < D ) -> ( D e. CC /\ D =/= 0 ) )
28 recdiv 
 |-  ( ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( 1 / ( C / D ) ) = ( D / C ) )
29 24 27 28 syl2an 
 |-  ( ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) -> ( 1 / ( C / D ) ) = ( D / C ) )
30 recn 
 |-  ( A e. RR -> A e. CC )
31 30 adantr 
 |-  ( ( A e. RR /\ 0 < A ) -> A e. CC )
32 gt0ne0 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
33 31 32 jca 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A e. CC /\ A =/= 0 ) )
34 recn 
 |-  ( B e. RR -> B e. CC )
35 34 adantr 
 |-  ( ( B e. RR /\ 0 < B ) -> B e. CC )
36 35 2 jca 
 |-  ( ( B e. RR /\ 0 < B ) -> ( B e. CC /\ B =/= 0 ) )
37 recdiv 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( 1 / ( A / B ) ) = ( B / A ) )
38 33 36 37 syl2an 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( 1 / ( A / B ) ) = ( B / A ) )
39 29 38 breqan12rd 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( 1 / ( C / D ) ) <_ ( 1 / ( A / B ) ) <-> ( D / C ) <_ ( B / A ) ) )
40 20 39 bitrd 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A / B ) <_ ( C / D ) <-> ( D / C ) <_ ( B / A ) ) )