Metamath Proof Explorer

Theorem lediv12a

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

Ref Expression
Assertion lediv12a ⊢A∈ℝ∧B∈ℝ∧0≤A∧A≤B∧C∈ℝ∧D∈ℝ∧0<C∧C≤D→AD≤BC

Proof

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