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

Metamath Proof Explorer

Theorem lediv12a

Description: Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> D e. RR )
2 0re 
 |-  0 e. RR
3 ltletr 
 |-  ( ( 0 e. RR /\ C e. RR /\ D e. RR ) -> ( ( 0 < C /\ C <_ D ) -> 0 < D ) )
4 2 3 mp3an1 
 |-  ( ( C e. RR /\ D e. RR ) -> ( ( 0 < C /\ C <_ D ) -> 0 < D ) )
5 4 imp 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> 0 < D )
6 5 gt0ne0d 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> D =/= 0 )
7 1 6 rereccld 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> ( 1 / D ) e. RR )
8 gt0ne0 
 |-  ( ( C e. RR /\ 0 < C ) -> C =/= 0 )
9 rereccl 
 |-  ( ( C e. RR /\ C =/= 0 ) -> ( 1 / C ) e. RR )
10 8 9 syldan 
 |-  ( ( C e. RR /\ 0 < C ) -> ( 1 / C ) e. RR )
11 10 ad2ant2r 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> ( 1 / C ) e. RR )
12 recgt0 
 |-  ( ( D e. RR /\ 0 < D ) -> 0 < ( 1 / D ) )
13 1 5 12 syl2anc 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> 0 < ( 1 / D ) )
14 ltle 
 |-  ( ( 0 e. RR /\ ( 1 / D ) e. RR ) -> ( 0 < ( 1 / D ) -> 0 <_ ( 1 / D ) ) )
15 2 7 14 sylancr 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> ( 0 < ( 1 / D ) -> 0 <_ ( 1 / D ) ) )
16 13 15 mpd 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> 0 <_ ( 1 / D ) )
17 simprr 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> C <_ D )
18 id 
 |-  ( ( C e. RR /\ 0 < C ) -> ( C e. RR /\ 0 < C ) )
19 18 ad2ant2r 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> ( C e. RR /\ 0 < C ) )
20 lerec 
 |-  ( ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) -> ( C <_ D <-> ( 1 / D ) <_ ( 1 / C ) ) )
21 19 1 5 20 syl12anc 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> ( C <_ D <-> ( 1 / D ) <_ ( 1 / C ) ) )
22 17 21 mpbid 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> ( 1 / D ) <_ ( 1 / C ) )
23 16 22 jca 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) )
24 7 11 23 jca31 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) )
25 simplll 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> A e. RR )
26 simplrl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> 0 <_ A )
27 simpllr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> B e. RR )
28 25 26 27 jca31 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) )
29 simprll 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> ( 1 / D ) e. RR )
30 simprrl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> 0 <_ ( 1 / D ) )
31 29 30 jca 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> ( ( 1 / D ) e. RR /\ 0 <_ ( 1 / D ) ) )
32 simprlr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> ( 1 / C ) e. RR )
33 28 31 32 jca32 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) /\ ( ( ( 1 / D ) e. RR /\ 0 <_ ( 1 / D ) ) /\ ( 1 / C ) e. RR ) ) )
34 simplrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> A <_ B )
35 simprrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> ( 1 / D ) <_ ( 1 / C ) )
36 34 35 jca 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> ( A <_ B /\ ( 1 / D ) <_ ( 1 / C ) ) )
37 lemul12a 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) /\ ( ( ( 1 / D ) e. RR /\ 0 <_ ( 1 / D ) ) /\ ( 1 / C ) e. RR ) ) -> ( ( A <_ B /\ ( 1 / D ) <_ ( 1 / C ) ) -> ( A x. ( 1 / D ) ) <_ ( B x. ( 1 / C ) ) ) )
38 33 36 37 sylc 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( ( 1 / D ) e. RR /\ ( 1 / C ) e. RR ) /\ ( 0 <_ ( 1 / D ) /\ ( 1 / D ) <_ ( 1 / C ) ) ) ) -> ( A x. ( 1 / D ) ) <_ ( B x. ( 1 / C ) ) )
39 24 38 sylan2 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( A x. ( 1 / D ) ) <_ ( B x. ( 1 / C ) ) )
40 recn 
 |-  ( A e. RR -> A e. CC )
41 40 adantr 
 |-  ( ( A e. RR /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> A e. CC )
42 recn 
 |-  ( D e. RR -> D e. CC )
43 42 ad2antlr 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) -> D e. CC )
44 43 adantl 
 |-  ( ( A e. RR /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> D e. CC )
45 6 adantl 
 |-  ( ( A e. RR /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> D =/= 0 )
46 41 44 45 divrecd 
 |-  ( ( A e. RR /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( A / D ) = ( A x. ( 1 / D ) ) )
47 46 ad4ant14 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( A / D ) = ( A x. ( 1 / D ) ) )
48 recn 
 |-  ( B e. RR -> B e. CC )
49 48 adantr 
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> B e. CC )
50 recn 
 |-  ( C e. RR -> C e. CC )
51 50 ad2antrl 
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C e. CC )
52 8 adantl 
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C =/= 0 )
53 49 51 52 divrecd 
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
54 53 adantrrr 
 |-  ( ( B e. RR /\ ( C e. RR /\ ( 0 < C /\ C <_ D ) ) ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
55 54 adantrlr 
 |-  ( ( B e. RR /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
56 55 ad4ant24 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
57 39 47 56 3brtr4d 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( A / D ) <_ ( B / C ) )