Step |
Hyp |
Ref |
Expression |
1 |
|
aks4d1p1p2.1 |
|
2 |
|
aks4d1p1p2.2 |
|
3 |
|
aks4d1p1p2.3 |
|
4 |
|
aks4d1p1p2.4 |
|
5 |
1
|
nnred |
|
6 |
|
2re |
|
7 |
6
|
a1i |
|
8 |
|
2pos |
|
9 |
8
|
a1i |
|
10 |
1
|
nngt0d |
|
11 |
|
1red |
|
12 |
|
1lt2 |
|
13 |
12
|
a1i |
|
14 |
11 13
|
ltned |
|
15 |
14
|
necomd |
|
16 |
7 9 5 10 15
|
relogbcld |
|
17 |
|
5nn0 |
|
18 |
17
|
a1i |
|
19 |
16 18
|
reexpcld |
|
20 |
|
ceilcl |
|
21 |
19 20
|
syl |
|
22 |
21
|
zred |
|
23 |
3
|
a1i |
|
24 |
23
|
eleq1d |
|
25 |
22 24
|
mpbird |
|
26 |
|
0red |
|
27 |
18
|
nn0zd |
|
28 |
|
3re |
|
29 |
28
|
a1i |
|
30 |
|
1lt3 |
|
31 |
30
|
a1i |
|
32 |
11 29 5 31 4
|
ltletrd |
|
33 |
5 10
|
elrpd |
|
34 |
|
2rp |
|
35 |
34 12
|
pm3.2i |
|
36 |
35
|
a1i |
|
37 |
|
logbgt0b |
|
38 |
33 36 37
|
syl2anc |
|
39 |
32 38
|
mpbird |
|
40 |
|
expgt0 |
|
41 |
16 27 39 40
|
syl3anc |
|
42 |
|
ceilge |
|
43 |
19 42
|
syl |
|
44 |
26 19 22 41 43
|
ltletrd |
|
45 |
23
|
breq2d |
|
46 |
44 45
|
mpbird |
|
47 |
7 9 25 46 15
|
relogbcld |
|
48 |
47
|
flcld |
|
49 |
|
7re |
|
50 |
49
|
a1i |
|
51 |
|
1lt7 |
|
52 |
51
|
a1i |
|
53 |
5 4
|
3lexlogpow5ineq3 |
|
54 |
11 50 19 52 53
|
lttrd |
|
55 |
11 19 22 54 43
|
ltletrd |
|
56 |
23
|
breq2d |
|
57 |
55 56
|
mpbird |
|
58 |
25 46
|
elrpd |
|
59 |
|
logbgt0b |
|
60 |
58 36 59
|
syl2anc |
|
61 |
57 60
|
mpbird |
|
62 |
26 47 61
|
ltled |
|
63 |
|
0zd |
|
64 |
|
flge |
|
65 |
47 63 64
|
syl2anc |
|
66 |
62 65
|
mpbid |
|
67 |
48 66
|
jca |
|
68 |
|
elnn0z |
|
69 |
67 68
|
sylibr |
|
70 |
5 69
|
reexpcld |
|
71 |
|
fzfid |
|
72 |
5
|
adantr |
|
73 |
|
elfznn |
|
74 |
73
|
adantl |
|
75 |
|
nnnn0 |
|
76 |
74 75
|
syl |
|
77 |
72 76
|
reexpcld |
|
78 |
|
1red |
|
79 |
77 78
|
resubcld |
|
80 |
71 79
|
fprodrecl |
|
81 |
70 80
|
remulcld |
|
82 |
2
|
a1i |
|
83 |
82
|
eleq1d |
|
84 |
81 83
|
mpbird |
|
85 |
1
|
nnnn0d |
|
86 |
85
|
nn0ge0d |
|
87 |
19 11
|
readdcld |
|
88 |
19
|
ltp1d |
|
89 |
26 19 87 41 88
|
lttrd |
|
90 |
7 9 87 89 15
|
relogbcld |
|
91 |
16
|
resqcld |
|
92 |
91
|
flcld |
|
93 |
92
|
zred |
|
94 |
|
0lt1 |
|
95 |
94
|
a1i |
|
96 |
7 9 7 9 15
|
relogbcld |
|
97 |
96
|
resqcld |
|
98 |
|
2nn0 |
|
99 |
98
|
a1i |
|
100 |
11
|
leidd |
|
101 |
7
|
recnd |
|
102 |
26 9
|
gtned |
|
103 |
|
logbid1 |
|
104 |
101 102 15 103
|
syl3anc |
|
105 |
104
|
eqcomd |
|
106 |
100 105
|
breqtrd |
|
107 |
96 99 106
|
expge1d |
|
108 |
105
|
eqcomd |
|
109 |
108
|
oveq1d |
|
110 |
99
|
nn0zd |
|
111 |
|
1exp |
|
112 |
110 111
|
syl |
|
113 |
109 112
|
eqtrd |
|
114 |
7
|
leidd |
|
115 |
|
1nn0 |
|
116 |
6 115
|
nn0addge1i |
|
117 |
|
2p1e3 |
|
118 |
116 117
|
breqtri |
|
119 |
118
|
a1i |
|
120 |
7 29 5 119 4
|
letrd |
|
121 |
110 114 7 9 5 10 120
|
logblebd |
|
122 |
11 96 16 106 121
|
letrd |
|
123 |
16 99 122
|
expge1d |
|
124 |
113 123
|
eqbrtrd |
|
125 |
|
1z |
|
126 |
|
zsqcl |
|
127 |
125 126
|
ax-mp |
|
128 |
127
|
a1i |
|
129 |
109
|
eleq1d |
|
130 |
128 129
|
mpbird |
|
131 |
91 130
|
jca |
|
132 |
|
flge |
|
133 |
131 132
|
syl |
|
134 |
124 133
|
mpbid |
|
135 |
11 97 93 107 134
|
letrd |
|
136 |
26 11 93 95 135
|
ltletrd |
|
137 |
92 136
|
jca |
|
138 |
|
elnnz |
|
139 |
138
|
bicomi |
|
140 |
139
|
a1i |
|
141 |
137 140
|
mpbid |
|
142 |
141
|
nnnn0d |
|
143 |
|
arisum |
|
144 |
142 143
|
syl |
|
145 |
74
|
nnred |
|
146 |
71 145
|
fsumrecl |
|
147 |
144 146
|
eqeltrrd |
|
148 |
90 147
|
readdcld |
|
149 |
5 86 148
|
recxpcld |
|
150 |
|
4nn0 |
|
151 |
150
|
a1i |
|
152 |
16 151
|
reexpcld |
|
153 |
152 91
|
readdcld |
|
154 |
153
|
rehalfcld |
|
155 |
90 154
|
readdcld |
|
156 |
5 86 155
|
recxpcld |
|
157 |
|
reflcl |
|
158 |
47 157
|
syl |
|
159 |
5 86 158
|
recxpcld |
|
160 |
33 146
|
rpcxpcld |
|
161 |
33 141
|
aks4d1p1p1 |
|
162 |
161
|
eleq1d |
|
163 |
160 162
|
mpbird |
|
164 |
163
|
rpregt0d |
|
165 |
164
|
simpld |
|
166 |
159 165
|
remulcld |
|
167 |
5 86 90
|
recxpcld |
|
168 |
167 165
|
remulcld |
|
169 |
71 77
|
fprodrecl |
|
170 |
5 69 86
|
expge0d |
|
171 |
|
nfv |
|
172 |
|
0red |
|
173 |
1
|
nnge1d |
|
174 |
173
|
adantr |
|
175 |
72 76 174
|
expge1d |
|
176 |
77
|
recnd |
|
177 |
176
|
subid1d |
|
178 |
177
|
breq2d |
|
179 |
175 178
|
mpbird |
|
180 |
78 77 172 179
|
lesubd |
|
181 |
77
|
lem1d |
|
182 |
171 71 79 180 77 181
|
fprodle |
|
183 |
80 169 70 170 182
|
lemul2ad |
|
184 |
82
|
breq1d |
|
185 |
183 184
|
mpbird |
|
186 |
72
|
recnd |
|
187 |
|
cxpexp |
|
188 |
186 76 187
|
syl2anc |
|
189 |
188
|
eqcomd |
|
190 |
189
|
prodeq2dv |
|
191 |
190
|
oveq2d |
|
192 |
185 191
|
breqtrd |
|
193 |
5
|
recnd |
|
194 |
|
cxpexp |
|
195 |
193 69 194
|
syl2anc |
|
196 |
195
|
oveq1d |
|
197 |
196
|
eqcomd |
|
198 |
192 197
|
breqtrd |
|
199 |
159 167 164
|
3jca |
|
200 |
1 3 4
|
aks4d1p1p3 |
|
201 |
|
ltmul1a |
|
202 |
199 200 201
|
syl2anc |
|
203 |
84 166 168 198 202
|
lelttrd |
|
204 |
161
|
oveq2d |
|
205 |
203 204
|
breqtrd |
|
206 |
144
|
oveq2d |
|
207 |
206
|
oveq2d |
|
208 |
205 207
|
breqtrd |
|
209 |
26 10
|
gtned |
|
210 |
90
|
recnd |
|
211 |
141
|
nncnd |
|
212 |
211
|
sqcld |
|
213 |
212 211
|
addcld |
|
214 |
213
|
halfcld |
|
215 |
193 209 210 214
|
cxpaddd |
|
216 |
215
|
eqcomd |
|
217 |
208 216
|
breqtrd |
|
218 |
|
reflcl |
|
219 |
91 218
|
syl |
|
220 |
219
|
resqcld |
|
221 |
220 219
|
readdcld |
|
222 |
34
|
a1i |
|
223 |
91 99
|
reexpcld |
|
224 |
|
id |
|
225 |
142
|
nn0ge0d |
|
226 |
|
flle |
|
227 |
91 226
|
syl |
|
228 |
219 91 99 225 227
|
leexp1ad |
|
229 |
224 228
|
syl |
|
230 |
16
|
recnd |
|
231 |
230 99 99
|
expmuld |
|
232 |
231
|
eqcomd |
|
233 |
|
2t2e4 |
|
234 |
233
|
oveq2i |
|
235 |
234
|
a1i |
|
236 |
232 235
|
eqtrd |
|
237 |
223 236
|
eqled |
|
238 |
220 223 152 229 237
|
letrd |
|
239 |
220 219 152 91 238 227
|
le2addd |
|
240 |
221 153 222 239
|
lediv1dd |
|
241 |
147 154 90 240
|
leadd2dd |
|
242 |
5 32 148 155
|
cxpled |
|
243 |
241 242
|
mpbid |
|
244 |
84 149 156 217 243
|
ltletrd |
|
245 |
152
|
recnd |
|
246 |
91
|
recnd |
|
247 |
245 246 101 102
|
divdird |
|
248 |
247
|
oveq2d |
|
249 |
248
|
oveq2d |
|
250 |
244 249
|
breqtrd |
|
251 |
245 101 102
|
divcld |
|
252 |
246 101 102
|
divcld |
|
253 |
251 252
|
addcomd |
|
254 |
253
|
oveq2d |
|
255 |
210 252 251
|
addassd |
|
256 |
255
|
eqcomd |
|
257 |
254 256
|
eqtrd |
|
258 |
257
|
oveq2d |
|
259 |
250 258
|
breqtrd |
|