Step |
Hyp |
Ref |
Expression |
1 |
|
qrng.q |
|
2 |
|
qabsabv.a |
|
3 |
|
padic.j |
|
4 |
|
ostth.k |
|
5 |
|
ostth.1 |
|
6 |
|
ostth3.2 |
|
7 |
|
ostth3.3 |
|
8 |
|
ostth3.4 |
|
9 |
|
ostth3.5 |
|
10 |
|
ostth3.6 |
|
11 |
|
prmuz2 |
|
12 |
7 11
|
syl |
|
13 |
|
eluz2b2 |
|
14 |
12 13
|
sylib |
|
15 |
14
|
simpld |
|
16 |
|
nnq |
|
17 |
15 16
|
syl |
|
18 |
1
|
qrngbas |
|
19 |
2 18
|
abvcl |
|
20 |
5 17 19
|
syl2anc |
|
21 |
15
|
nnne0d |
|
22 |
1
|
qrng0 |
|
23 |
2 18 22
|
abvgt0 |
|
24 |
5 17 21 23
|
syl3anc |
|
25 |
20 24
|
elrpd |
|
26 |
25
|
relogcld |
|
27 |
15
|
nnred |
|
28 |
14
|
simprd |
|
29 |
27 28
|
rplogcld |
|
30 |
26 29
|
rerpdivcld |
|
31 |
30
|
renegcld |
|
32 |
9 31
|
eqeltrid |
|
33 |
|
1rp |
|
34 |
|
logltb |
|
35 |
25 33 34
|
sylancl |
|
36 |
8 35
|
mpbid |
|
37 |
|
log1 |
|
38 |
36 37
|
breqtrdi |
|
39 |
29
|
rpcnd |
|
40 |
39
|
mul01d |
|
41 |
38 40
|
breqtrrd |
|
42 |
|
0red |
|
43 |
26 42 29
|
ltdivmuld |
|
44 |
41 43
|
mpbird |
|
45 |
30
|
lt0neg1d |
|
46 |
44 45
|
mpbid |
|
47 |
46 9
|
breqtrrdi |
|
48 |
32 47
|
elrpd |
|
49 |
1 2 3
|
padicabvcxp |
|
50 |
7 48 49
|
syl2anc |
|
51 |
|
fveq2 |
|
52 |
51
|
oveq1d |
|
53 |
|
eqid |
|
54 |
|
ovex |
|
55 |
52 53 54
|
fvmpt |
|
56 |
17 55
|
syl |
|
57 |
3
|
padicval |
|
58 |
7 17 57
|
syl2anc |
|
59 |
21
|
neneqd |
|
60 |
59
|
iffalsed |
|
61 |
15
|
nncnd |
|
62 |
61
|
exp1d |
|
63 |
62
|
oveq2d |
|
64 |
|
1z |
|
65 |
|
pcid |
|
66 |
7 64 65
|
sylancl |
|
67 |
63 66
|
eqtr3d |
|
68 |
67
|
negeqd |
|
69 |
68
|
oveq2d |
|
70 |
|
neg1z |
|
71 |
70
|
a1i |
|
72 |
61 21 71
|
cxpexpzd |
|
73 |
69 72
|
eqtr4d |
|
74 |
58 60 73
|
3eqtrd |
|
75 |
74
|
oveq1d |
|
76 |
32
|
recnd |
|
77 |
76
|
mulm1d |
|
78 |
9
|
negeqi |
|
79 |
30
|
recnd |
|
80 |
79
|
negnegd |
|
81 |
78 80
|
eqtrid |
|
82 |
77 81
|
eqtrd |
|
83 |
82
|
oveq2d |
|
84 |
15
|
nnrpd |
|
85 |
|
neg1rr |
|
86 |
85
|
a1i |
|
87 |
84 86 76
|
cxpmuld |
|
88 |
61 21 79
|
cxpefd |
|
89 |
26
|
recnd |
|
90 |
29
|
rpne0d |
|
91 |
89 39 90
|
divcan1d |
|
92 |
91
|
fveq2d |
|
93 |
25
|
reeflogd |
|
94 |
88 92 93
|
3eqtrd |
|
95 |
83 87 94
|
3eqtr3d |
|
96 |
56 75 95
|
3eqtrrd |
|
97 |
|
fveq2 |
|
98 |
|
fveq2 |
|
99 |
97 98
|
eqeq12d |
|
100 |
96 99
|
syl5ibcom |
|
101 |
100
|
adantr |
|
102 |
|
prmnn |
|
103 |
102
|
ad2antlr |
|
104 |
|
nnq |
|
105 |
103 104
|
syl |
|
106 |
|
fveq2 |
|
107 |
106
|
oveq1d |
|
108 |
|
ovex |
|
109 |
107 53 108
|
fvmpt |
|
110 |
105 109
|
syl |
|
111 |
76
|
ad2antrr |
|
112 |
111
|
1cxpd |
|
113 |
7
|
ad2antrr |
|
114 |
3
|
padicval |
|
115 |
113 105 114
|
syl2anc |
|
116 |
103
|
nnne0d |
|
117 |
116
|
neneqd |
|
118 |
117
|
iffalsed |
|
119 |
|
pceq0 |
|
120 |
7 102 119
|
syl2an |
|
121 |
|
dvdsprm |
|
122 |
12 121
|
sylan |
|
123 |
122
|
necon3bbid |
|
124 |
120 123
|
bitrd |
|
125 |
124
|
biimpar |
|
126 |
125
|
negeqd |
|
127 |
|
neg0 |
|
128 |
126 127
|
eqtrdi |
|
129 |
128
|
oveq2d |
|
130 |
61
|
ad2antrr |
|
131 |
130
|
exp0d |
|
132 |
129 131
|
eqtrd |
|
133 |
115 118 132
|
3eqtrd |
|
134 |
133
|
oveq1d |
|
135 |
|
2re |
|
136 |
135
|
a1i |
|
137 |
5
|
ad2antrr |
|
138 |
2 18
|
abvcl |
|
139 |
137 105 138
|
syl2anc |
|
140 |
2 18 22
|
abvgt0 |
|
141 |
137 105 116 140
|
syl3anc |
|
142 |
139 141
|
elrpd |
|
143 |
142
|
adantrr |
|
144 |
25
|
ad2antrr |
|
145 |
143 144
|
ifcld |
|
146 |
10 145
|
eqeltrid |
|
147 |
146
|
rprecred |
|
148 |
|
simprr |
|
149 |
8
|
ad2antrr |
|
150 |
|
breq1 |
|
151 |
|
breq1 |
|
152 |
150 151
|
ifboth |
|
153 |
148 149 152
|
syl2anc |
|
154 |
10 153
|
eqbrtrid |
|
155 |
146
|
reclt1d |
|
156 |
154 155
|
mpbid |
|
157 |
|
expnbnd |
|
158 |
136 147 156 157
|
syl3anc |
|
159 |
146
|
rpcnd |
|
160 |
159
|
adantr |
|
161 |
146
|
rpne0d |
|
162 |
161
|
adantr |
|
163 |
|
nnz |
|
164 |
163
|
adantl |
|
165 |
160 162 164
|
exprecd |
|
166 |
5
|
ad3antrrr |
|
167 |
|
ax-1ne0 |
|
168 |
1
|
qrng1 |
|
169 |
2 168 22
|
abv1z |
|
170 |
166 167 169
|
sylancl |
|
171 |
15
|
ad2antrr |
|
172 |
|
nnnn0 |
|
173 |
|
nnexpcl |
|
174 |
171 172 173
|
syl2an |
|
175 |
174
|
nnzd |
|
176 |
102
|
ad2antlr |
|
177 |
|
nnexpcl |
|
178 |
176 172 177
|
syl2an |
|
179 |
178
|
nnzd |
|
180 |
|
bezout |
|
181 |
175 179 180
|
syl2anc |
|
182 |
|
simprl |
|
183 |
7
|
ad2antrr |
|
184 |
|
simplr |
|
185 |
|
prmrp |
|
186 |
183 184 185
|
syl2anc |
|
187 |
182 186
|
mpbird |
|
188 |
187
|
adantr |
|
189 |
171
|
adantr |
|
190 |
176
|
adantr |
|
191 |
|
simpr |
|
192 |
|
rppwr |
|
193 |
189 190 191 192
|
syl3anc |
|
194 |
188 193
|
mpd |
|
195 |
194
|
adantrr |
|
196 |
195
|
eqeq1d |
|
197 |
5
|
ad3antrrr |
|
198 |
174
|
adantrr |
|
199 |
|
nnq |
|
200 |
198 199
|
syl |
|
201 |
|
simprrl |
|
202 |
|
zq |
|
203 |
201 202
|
syl |
|
204 |
|
qmulcl |
|
205 |
200 203 204
|
syl2anc |
|
206 |
178
|
adantrr |
|
207 |
|
nnq |
|
208 |
206 207
|
syl |
|
209 |
|
simprrr |
|
210 |
|
zq |
|
211 |
209 210
|
syl |
|
212 |
|
qmulcl |
|
213 |
208 211 212
|
syl2anc |
|
214 |
|
qaddcl |
|
215 |
205 213 214
|
syl2anc |
|
216 |
2 18
|
abvcl |
|
217 |
197 215 216
|
syl2anc |
|
218 |
2 18
|
abvcl |
|
219 |
197 205 218
|
syl2anc |
|
220 |
2 18
|
abvcl |
|
221 |
197 213 220
|
syl2anc |
|
222 |
219 221
|
readdcld |
|
223 |
|
rpexpcl |
|
224 |
146 163 223
|
syl2an |
|
225 |
224
|
rpred |
|
226 |
225
|
adantrr |
|
227 |
|
remulcl |
|
228 |
135 226 227
|
sylancr |
|
229 |
|
qex |
|
230 |
|
cnfldadd |
|
231 |
1 230
|
ressplusg |
|
232 |
229 231
|
ax-mp |
|
233 |
2 18 232
|
abvtri |
|
234 |
197 205 213 233
|
syl3anc |
|
235 |
|
cnfldmul |
|
236 |
1 235
|
ressmulr |
|
237 |
229 236
|
ax-mp |
|
238 |
2 18 237
|
abvmul |
|
239 |
197 200 203 238
|
syl3anc |
|
240 |
17
|
ad3antrrr |
|
241 |
172
|
ad2antrl |
|
242 |
1 2
|
qabvexp |
|
243 |
197 240 241 242
|
syl3anc |
|
244 |
243
|
oveq1d |
|
245 |
239 244
|
eqtrd |
|
246 |
197 240 19
|
syl2anc |
|
247 |
246 241
|
reexpcld |
|
248 |
2 18
|
abvcl |
|
249 |
197 203 248
|
syl2anc |
|
250 |
247 249
|
remulcld |
|
251 |
|
elz |
|
252 |
251
|
simprbi |
|
253 |
252
|
adantl |
|
254 |
2 22
|
abv0 |
|
255 |
5 254
|
syl |
|
256 |
|
0le1 |
|
257 |
255 256
|
eqbrtrdi |
|
258 |
257
|
adantr |
|
259 |
|
fveq2 |
|
260 |
259
|
breq1d |
|
261 |
258 260
|
syl5ibrcom |
|
262 |
|
nnq |
|
263 |
2 18
|
abvcl |
|
264 |
5 262 263
|
syl2an |
|
265 |
|
1re |
|
266 |
|
lenlt |
|
267 |
264 265 266
|
sylancl |
|
268 |
267
|
ralbidva |
|
269 |
6 268
|
mpbird |
|
270 |
|
fveq2 |
|
271 |
270
|
breq1d |
|
272 |
271
|
rspccv |
|
273 |
269 272
|
syl |
|
274 |
273
|
adantr |
|
275 |
5
|
adantr |
|
276 |
202
|
ad2antrl |
|
277 |
|
eqid |
|
278 |
2 18 277
|
abvneg |
|
279 |
275 276 278
|
syl2anc |
|
280 |
|
fveq2 |
|
281 |
280
|
breq1d |
|
282 |
269
|
adantr |
|
283 |
1
|
qrngneg |
|
284 |
276 283
|
syl |
|
285 |
|
simprr |
|
286 |
284 285
|
eqeltrd |
|
287 |
281 282 286
|
rspcdva |
|
288 |
279 287
|
eqbrtrrd |
|
289 |
288
|
expr |
|
290 |
261 274 289
|
3jaod |
|
291 |
253 290
|
mpd |
|
292 |
291
|
ralrimiva |
|
293 |
292
|
ad3antrrr |
|
294 |
|
rsp |
|
295 |
293 201 294
|
sylc |
|
296 |
265
|
a1i |
|
297 |
163
|
ad2antrl |
|
298 |
24
|
ad3antrrr |
|
299 |
|
expgt0 |
|
300 |
246 297 298 299
|
syl3anc |
|
301 |
|
lemul2 |
|
302 |
249 296 247 300 301
|
syl112anc |
|
303 |
295 302
|
mpbid |
|
304 |
247
|
recnd |
|
305 |
304
|
mulid1d |
|
306 |
303 305
|
breqtrd |
|
307 |
146
|
rpred |
|
308 |
307
|
adantr |
|
309 |
144
|
adantr |
|
310 |
309
|
rpge0d |
|
311 |
176
|
adantr |
|
312 |
311 104
|
syl |
|
313 |
197 312 138
|
syl2anc |
|
314 |
|
max1 |
|
315 |
246 313 314
|
syl2anc |
|
316 |
315 10
|
breqtrrdi |
|
317 |
|
leexp1a |
|
318 |
246 308 241 310 316 317
|
syl32anc |
|
319 |
250 247 226 306 318
|
letrd |
|
320 |
245 319
|
eqbrtrd |
|
321 |
2 18 237
|
abvmul |
|
322 |
197 208 211 321
|
syl3anc |
|
323 |
1 2
|
qabvexp |
|
324 |
197 312 241 323
|
syl3anc |
|
325 |
324
|
oveq1d |
|
326 |
322 325
|
eqtrd |
|
327 |
313 241
|
reexpcld |
|
328 |
2 18
|
abvcl |
|
329 |
197 211 328
|
syl2anc |
|
330 |
327 329
|
remulcld |
|
331 |
|
fveq2 |
|
332 |
331
|
breq1d |
|
333 |
332 293 209
|
rspcdva |
|
334 |
311
|
nnne0d |
|
335 |
197 312 334 140
|
syl3anc |
|
336 |
|
expgt0 |
|
337 |
313 297 335 336
|
syl3anc |
|
338 |
|
lemul2 |
|
339 |
329 296 327 337 338
|
syl112anc |
|
340 |
333 339
|
mpbid |
|
341 |
327
|
recnd |
|
342 |
341
|
mulid1d |
|
343 |
340 342
|
breqtrd |
|
344 |
143
|
adantr |
|
345 |
344
|
rpge0d |
|
346 |
|
max2 |
|
347 |
246 313 346
|
syl2anc |
|
348 |
347 10
|
breqtrrdi |
|
349 |
|
leexp1a |
|
350 |
313 308 241 345 348 349
|
syl32anc |
|
351 |
330 327 226 343 350
|
letrd |
|
352 |
326 351
|
eqbrtrd |
|
353 |
219 221 226 226 320 352
|
le2addd |
|
354 |
224
|
rpcnd |
|
355 |
354
|
2timesd |
|
356 |
355
|
adantrr |
|
357 |
353 356
|
breqtrrd |
|
358 |
217 222 228 234 357
|
letrd |
|
359 |
|
fveq2 |
|
360 |
359
|
breq1d |
|
361 |
358 360
|
syl5ibrcom |
|
362 |
196 361
|
sylbid |
|
363 |
362
|
anassrs |
|
364 |
363
|
rexlimdvva |
|
365 |
181 364
|
mpd |
|
366 |
170 365
|
eqbrtrrd |
|
367 |
224
|
rpregt0d |
|
368 |
|
ledivmul2 |
|
369 |
265 135 367 368
|
mp3an12i |
|
370 |
366 369
|
mpbird |
|
371 |
165 370
|
eqbrtrd |
|
372 |
|
reexpcl |
|
373 |
147 172 372
|
syl2an |
|
374 |
|
lenlt |
|
375 |
373 135 374
|
sylancl |
|
376 |
371 375
|
mpbid |
|
377 |
376
|
pm2.21d |
|
378 |
377
|
rexlimdva |
|
379 |
158 378
|
mpd |
|
380 |
379
|
expr |
|
381 |
380
|
pm2.01d |
|
382 |
|
fveq2 |
|
383 |
382
|
breq2d |
|
384 |
383
|
notbid |
|
385 |
6
|
ad2antrr |
|
386 |
384 385 103
|
rspcdva |
|
387 |
|
lttri3 |
|
388 |
139 265 387
|
sylancl |
|
389 |
381 386 388
|
mpbir2and |
|
390 |
112 134 389
|
3eqtr4d |
|
391 |
110 390
|
eqtr2d |
|
392 |
391
|
ex |
|
393 |
101 392
|
pm2.61dne |
|
394 |
1 2 5 50 393
|
ostthlem2 |
|
395 |
|
oveq2 |
|
396 |
395
|
mpteq2dv |
|
397 |
396
|
rspceeqv |
|
398 |
48 394 397
|
syl2anc |
|