Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . 6
|
2 | 1 | rpreccld 11882 |
. . . . 5
|
3 | 2 | rprege0d 11879 |
. . . 4
|
4 | | flge0nn0 12621 |
. . . 4
|
5 | | nn0p1nn 11332 |
. . . 4
|
6 | 3, 4, 5 | 3syl 18 |
. . 3
|
7 | | irrapxlem4 37389 |
. . 3
|
8 | 6, 7 | syldan 487 |
. 2
|
9 | | simplrr 801 |
. . . . . . 7
|
10 | | nnq 11801 |
. . . . . . 7
|
11 | 9, 10 | syl 17 |
. . . . . 6
|
12 | | simplrl 800 |
. . . . . . 7
|
13 | | nnq 11801 |
. . . . . . 7
|
14 | 12, 13 | syl 17 |
. . . . . 6
|
15 | 12 | nnne0d 11065 |
. . . . . 6
|
16 | | qdivcl 11809 |
. . . . . 6
|
17 | 11, 14, 15, 16 | syl3anc 1326 |
. . . . 5
|
18 | 9 | nnrpd 11870 |
. . . . . . 7
|
19 | 12 | nnrpd 11870 |
. . . . . . 7
|
20 | 18, 19 | rpdivcld 11889 |
. . . . . 6
|
21 | 20 | rpgt0d 11875 |
. . . . 5
|
22 | 12 | nnred 11035 |
. . . . . . . . . . . 12
|
23 | 12 | nnnn0d 11351 |
. . . . . . . . . . . . 13
|
24 | 23 | nn0ge0d 11354 |
. . . . . . . . . . . 12
|
25 | 22, 24 | absidd 14161 |
. . . . . . . . . . 11
|
26 | 25 | eqcomd 2628 |
. . . . . . . . . 10
|
27 | 26 | oveq1d 6665 |
. . . . . . . . 9
|
28 | 12 | nncnd 11036 |
. . . . . . . . . 10
|
29 | | qre 11793 |
. . . . . . . . . . . . 13
|
30 | 17, 29 | syl 17 |
. . . . . . . . . . . 12
|
31 | | rpre 11839 |
. . . . . . . . . . . . 13
|
32 | 31 | ad3antrrr 766 |
. . . . . . . . . . . 12
|
33 | 30, 32 | resubcld 10458 |
. . . . . . . . . . 11
|
34 | 33 | recnd 10068 |
. . . . . . . . . 10
|
35 | 28, 34 | absmuld 14193 |
. . . . . . . . 9
|
36 | 27, 35 | eqtr4d 2659 |
. . . . . . . 8
|
37 | | qcn 11802 |
. . . . . . . . . . . 12
|
38 | 17, 37 | syl 17 |
. . . . . . . . . . 11
|
39 | | rpcn 11841 |
. . . . . . . . . . . 12
|
40 | 39 | ad3antrrr 766 |
. . . . . . . . . . 11
|
41 | 28, 38, 40 | subdid 10486 |
. . . . . . . . . 10
|
42 | 9 | nncnd 11036 |
. . . . . . . . . . . 12
|
43 | 42, 28, 15 | divcan2d 10803 |
. . . . . . . . . . 11
|
44 | 28, 40 | mulcomd 10061 |
. . . . . . . . . . 11
|
45 | 43, 44 | oveq12d 6668 |
. . . . . . . . . 10
|
46 | 41, 45 | eqtrd 2656 |
. . . . . . . . 9
|
47 | 46 | fveq2d 6195 |
. . . . . . . 8
|
48 | 32, 22 | remulcld 10070 |
. . . . . . . . . 10
|
49 | 48 | recnd 10068 |
. . . . . . . . 9
|
50 | 42, 49 | abssubd 14192 |
. . . . . . . 8
|
51 | 36, 47, 50 | 3eqtrd 2660 |
. . . . . . 7
|
52 | 9 | nnred 11035 |
. . . . . . . . . . 11
|
53 | 48, 52 | resubcld 10458 |
. . . . . . . . . 10
|
54 | 53 | recnd 10068 |
. . . . . . . . 9
|
55 | 54 | abscld 14175 |
. . . . . . . 8
|
56 | | simpllr 799 |
. . . . . . . . . . . . . 14
|
57 | 56 | rprecred 11883 |
. . . . . . . . . . . . 13
|
58 | 56 | rpreccld 11882 |
. . . . . . . . . . . . . 14
|
59 | 58 | rpge0d 11876 |
. . . . . . . . . . . . 13
|
60 | 57, 59, 4 | syl2anc 693 |
. . . . . . . . . . . 12
|
61 | 60, 5 | syl 17 |
. . . . . . . . . . 11
|
62 | 61 | nnrpd 11870 |
. . . . . . . . . 10
|
63 | 62, 19 | ifcld 4131 |
. . . . . . . . 9
|
64 | 63 | rprecred 11883 |
. . . . . . . 8
|
65 | 56 | rpred 11872 |
. . . . . . . . 9
|
66 | 22, 65 | remulcld 10070 |
. . . . . . . 8
|
67 | | simpr 477 |
. . . . . . . 8
|
68 | 58 | rprecred 11883 |
. . . . . . . . 9
|
69 | 61 | nnred 11035 |
. . . . . . . . . . 11
|
70 | 69, 22 | ifcld 4131 |
. . . . . . . . . . 11
|
71 | | fllep1 12602 |
. . . . . . . . . . . 12
|
72 | 57, 71 | syl 17 |
. . . . . . . . . . 11
|
73 | | max2 12018 |
. . . . . . . . . . . 12
|
74 | 22, 69, 73 | syl2anc 693 |
. . . . . . . . . . 11
|
75 | 57, 69, 70, 72, 74 | letrd 10194 |
. . . . . . . . . 10
|
76 | 58, 63 | lerecd 11891 |
. . . . . . . . . 10
|
77 | 75, 76 | mpbid 222 |
. . . . . . . . 9
|
78 | 65 | recnd 10068 |
. . . . . . . . . . . 12
|
79 | 56 | rpne0d 11877 |
. . . . . . . . . . . 12
|
80 | 78, 79 | recrecd 10798 |
. . . . . . . . . . 11
|
81 | 78 | mulid2d 10058 |
. . . . . . . . . . 11
|
82 | 80, 81 | eqtr4d 2659 |
. . . . . . . . . 10
|
83 | 12 | nnge1d 11063 |
. . . . . . . . . . 11
|
84 | | 1red 10055 |
. . . . . . . . . . . 12
|
85 | 84, 22, 56 | lemul1d 11915 |
. . . . . . . . . . 11
|
86 | 83, 85 | mpbid 222 |
. . . . . . . . . 10
|
87 | 82, 86 | eqbrtrd 4675 |
. . . . . . . . 9
|
88 | 64, 68, 66, 77, 87 | letrd 10194 |
. . . . . . . 8
|
89 | 55, 64, 66, 67, 88 | ltletrd 10197 |
. . . . . . 7
|
90 | 51, 89 | eqbrtrd 4675 |
. . . . . 6
|
91 | 34 | abscld 14175 |
. . . . . . 7
|
92 | 12 | nngt0d 11064 |
. . . . . . 7
|
93 | | ltmul2 10874 |
. . . . . . 7
|
94 | 91, 65, 22, 92, 93 | syl112anc 1330 |
. . . . . 6
|
95 | 90, 94 | mpbird 247 |
. . . . 5
|
96 | 22, 22 | remulcld 10070 |
. . . . . . . 8
|
97 | 22, 15 | msqgt0d 10595 |
. . . . . . . . 9
|
98 | 97 | gt0ne0d 10592 |
. . . . . . . 8
|
99 | 96, 98 | rereccld 10852 |
. . . . . . 7
|
100 | | qdencl 15449 |
. . . . . . . . . . 11
denom |
101 | 17, 100 | syl 17 |
. . . . . . . . . 10
denom |
102 | 101 | nnred 11035 |
. . . . . . . . 9
denom |
103 | 102, 102 | remulcld 10070 |
. . . . . . . 8
denom denom |
104 | 101 | nnne0d 11065 |
. . . . . . . . . 10
denom |
105 | 102, 104 | msqgt0d 10595 |
. . . . . . . . 9
denom denom |
106 | 105 | gt0ne0d 10592 |
. . . . . . . 8
denom denom |
107 | 103, 106 | rereccld 10852 |
. . . . . . 7
denom denom |
108 | 22, 15 | rereccld 10852 |
. . . . . . . . . 10
|
109 | | max1 12016 |
. . . . . . . . . . . 12
|
110 | 22, 69, 109 | syl2anc 693 |
. . . . . . . . . . 11
|
111 | 19, 63 | lerecd 11891 |
. . . . . . . . . . 11
|
112 | 110, 111 | mpbid 222 |
. . . . . . . . . 10
|
113 | 55, 64, 108, 67, 112 | ltletrd 10197 |
. . . . . . . . 9
|
114 | 28, 28, 28, 15, 15 | divdiv1d 10832 |
. . . . . . . . . 10
|
115 | 28, 15 | dividd 10799 |
. . . . . . . . . . 11
|
116 | 115 | oveq1d 6665 |
. . . . . . . . . 10
|
117 | 96 | recnd 10068 |
. . . . . . . . . . 11
|
118 | 28, 117, 98 | divrecd 10804 |
. . . . . . . . . 10
|
119 | 114, 116,
118 | 3eqtr3rd 2665 |
. . . . . . . . 9
|
120 | 113, 51, 119 | 3brtr4d 4685 |
. . . . . . . 8
|
121 | | ltmul2 10874 |
. . . . . . . . 9
|
122 | 91, 99, 22, 92, 121 | syl112anc 1330 |
. . . . . . . 8
|
123 | 120, 122 | mpbird 247 |
. . . . . . 7
|
124 | 9 | nnzd 11481 |
. . . . . . . . . 10
|
125 | | divdenle 15457 |
. . . . . . . . . 10
denom |
126 | 124, 12, 125 | syl2anc 693 |
. . . . . . . . 9
denom |
127 | 101 | nnnn0d 11351 |
. . . . . . . . . . 11
denom |
128 | 127 | nn0ge0d 11354 |
. . . . . . . . . 10
denom |
129 | | le2msq 10923 |
. . . . . . . . . 10
denom denom denom denom denom |
130 | 102, 128,
22, 24, 129 | syl22anc 1327 |
. . . . . . . . 9
denom
denom denom |
131 | 126, 130 | mpbid 222 |
. . . . . . . 8
denom denom |
132 | | lerec 10906 |
. . . . . . . . 9
denom denom denom denom denom denom denom denom |
133 | 103, 105,
96, 97, 132 | syl22anc 1327 |
. . . . . . . 8
denom denom denom denom |
134 | 131, 133 | mpbid 222 |
. . . . . . 7
denom denom |
135 | 91, 99, 107, 123, 134 | ltletrd 10197 |
. . . . . 6
denom denom |
136 | 101 | nncnd 11036 |
. . . . . . . 8
denom |
137 | | 2nn0 11309 |
. . . . . . . 8
|
138 | | expneg 12868 |
. . . . . . . 8
denom denom denom |
139 | 136, 137,
138 | sylancl 694 |
. . . . . . 7
denom denom |
140 | 136 | sqvald 13005 |
. . . . . . . 8
denom denom denom |
141 | 140 | oveq2d 6666 |
. . . . . . 7
denom denom denom |
142 | 139, 141 | eqtrd 2656 |
. . . . . 6
denom denom denom |
143 | 135, 142 | breqtrrd 4681 |
. . . . 5
denom |
144 | | breq2 4657 |
. . . . . . 7
|
145 | | oveq1 6657 |
. . . . . . . . 9
|
146 | 145 | fveq2d 6195 |
. . . . . . . 8
|
147 | 146 | breq1d 4663 |
. . . . . . 7
|
148 | | fveq2 6191 |
. . . . . . . . 9
denom denom |
149 | 148 | oveq1d 6665 |
. . . . . . . 8
denom denom |
150 | 146, 149 | breq12d 4666 |
. . . . . . 7
denom denom |
151 | 144, 147,
150 | 3anbi123d 1399 |
. . . . . 6
denom
denom |
152 | 151 | rspcev 3309 |
. . . . 5
denom
denom |
153 | 17, 21, 95, 143, 152 | syl13anc 1328 |
. . . 4
denom |
154 | 153 | ex 450 |
. . 3
denom |
155 | 154 | rexlimdvva 3038 |
. 2
denom |
156 | 8, 155 | mpd 15 |
1
denom |