Metamath Proof Explorer

Theorem lediv12a

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

Ref Expression
Assertion lediv12a ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ ( 0 < 𝐶 ∧ 𝐶 ≤ 𝐷 ) ) ) → ( 𝐴 / 𝐷 ) ≤ ( 𝐵 / 𝐶 ) )

Proof

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