Metamath Proof Explorer


Theorem lediv12a

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

Ref Expression
Assertion lediv12a AB0AABCD0<CCDADBC

Proof

Step Hyp Ref Expression
1 simplr CD0<CCDD
2 0re 0
3 ltletr 0CD0<CCD0<D
4 2 3 mp3an1 CD0<CCD0<D
5 4 imp CD0<CCD0<D
6 5 gt0ne0d CD0<CCDD0
7 1 6 rereccld CD0<CCD1D
8 gt0ne0 C0<CC0
9 rereccl CC01C
10 8 9 syldan C0<C1C
11 10 ad2ant2r CD0<CCD1C
12 recgt0 D0<D0<1D
13 1 5 12 syl2anc CD0<CCD0<1D
14 ltle 01D0<1D01D
15 2 7 14 sylancr CD0<CCD0<1D01D
16 13 15 mpd CD0<CCD01D
17 simprr CD0<CCDCD
18 id C0<CC0<C
19 18 ad2ant2r CD0<CCDC0<C
20 lerec C0<CD0<DCD1D1C
21 19 1 5 20 syl12anc CD0<CCDCD1D1C
22 17 21 mpbid CD0<CCD1D1C
23 16 22 jca CD0<CCD01D1D1C
24 7 11 23 jca31 CD0<CCD1D1C01D1D1C
25 simplll AB0AAB1D1C01D1D1CA
26 simplrl AB0AAB1D1C01D1D1C0A
27 simpllr AB0AAB1D1C01D1D1CB
28 25 26 27 jca31 AB0AAB1D1C01D1D1CA0AB
29 simprll AB0AAB1D1C01D1D1C1D
30 simprrl AB0AAB1D1C01D1D1C01D
31 29 30 jca AB0AAB1D1C01D1D1C1D01D
32 simprlr AB0AAB1D1C01D1D1C1C
33 28 31 32 jca32 AB0AAB1D1C01D1D1CA0AB1D01D1C
34 simplrr AB0AAB1D1C01D1D1CAB
35 simprrr AB0AAB1D1C01D1D1C1D1C
36 34 35 jca AB0AAB1D1C01D1D1CAB1D1C
37 lemul12a A0AB1D01D1CAB1D1CA1DB1C
38 33 36 37 sylc AB0AAB1D1C01D1D1CA1DB1C
39 24 38 sylan2 AB0AABCD0<CCDA1DB1C
40 recn AA
41 40 adantr ACD0<CCDA
42 recn DD
43 42 ad2antlr CD0<CCDD
44 43 adantl ACD0<CCDD
45 6 adantl ACD0<CCDD0
46 41 44 45 divrecd ACD0<CCDAD=A1D
47 46 ad4ant14 AB0AABCD0<CCDAD=A1D
48 recn BB
49 48 adantr BC0<CB
50 recn CC
51 50 ad2antrl BC0<CC
52 8 adantl BC0<CC0
53 49 51 52 divrecd BC0<CBC=B1C
54 53 adantrrr BC0<CCDBC=B1C
55 54 adantrlr BCD0<CCDBC=B1C
56 55 ad4ant24 AB0AABCD0<CCDBC=B1C
57 39 47 56 3brtr4d AB0AABCD0<CCDADBC