Description: Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | lediv12a | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplr | |
|
2 | 0re | |
|
3 | ltletr | |
|
4 | 2 3 | mp3an1 | |
5 | 4 | imp | |
6 | 5 | gt0ne0d | |
7 | 1 6 | rereccld | |
8 | gt0ne0 | |
|
9 | rereccl | |
|
10 | 8 9 | syldan | |
11 | 10 | ad2ant2r | |
12 | recgt0 | |
|
13 | 1 5 12 | syl2anc | |
14 | ltle | |
|
15 | 2 7 14 | sylancr | |
16 | 13 15 | mpd | |
17 | simprr | |
|
18 | id | |
|
19 | 18 | ad2ant2r | |
20 | lerec | |
|
21 | 19 1 5 20 | syl12anc | |
22 | 17 21 | mpbid | |
23 | 16 22 | jca | |
24 | 7 11 23 | jca31 | |
25 | simplll | |
|
26 | simplrl | |
|
27 | simpllr | |
|
28 | 25 26 27 | jca31 | |
29 | simprll | |
|
30 | simprrl | |
|
31 | 29 30 | jca | |
32 | simprlr | |
|
33 | 28 31 32 | jca32 | |
34 | simplrr | |
|
35 | simprrr | |
|
36 | 34 35 | jca | |
37 | lemul12a | |
|
38 | 33 36 37 | sylc | |
39 | 24 38 | sylan2 | |
40 | recn | |
|
41 | 40 | adantr | |
42 | recn | |
|
43 | 42 | ad2antlr | |
44 | 43 | adantl | |
45 | 6 | adantl | |
46 | 41 44 45 | divrecd | |
47 | 46 | ad4ant14 | |
48 | recn | |
|
49 | 48 | adantr | |
50 | recn | |
|
51 | 50 | ad2antrl | |
52 | 8 | adantl | |
53 | 49 51 52 | divrecd | |
54 | 53 | adantrrr | |
55 | 54 | adantrlr | |
56 | 55 | ad4ant24 | |
57 | 39 47 56 | 3brtr4d | |