Step |
Hyp |
Ref |
Expression |
1 |
|
fouriersw.t |
|
2 |
|
fouriersw.f |
|
3 |
|
fouriersw.x |
|
4 |
|
fouriersw.z |
|
5 |
|
fouriersw.y |
|
6 |
|
nnuz |
|
7 |
|
1zzd |
|
8 |
|
eqidd |
|
9 |
|
oveq2 |
|
10 |
9
|
oveq1d |
|
11 |
10
|
oveq1d |
|
12 |
11
|
fveq2d |
|
13 |
12 10
|
oveq12d |
|
14 |
13
|
adantl |
|
15 |
|
id |
|
16 |
|
ovex |
|
17 |
16
|
a1i |
|
18 |
8 14 15 17
|
fvmptd |
|
19 |
18
|
adantl |
|
20 |
|
2z |
|
21 |
20
|
a1i |
|
22 |
|
nnz |
|
23 |
21 22
|
zmulcld |
|
24 |
|
1zzd |
|
25 |
23 24
|
zsubcld |
|
26 |
25
|
zcnd |
|
27 |
3
|
recni |
|
28 |
27
|
a1i |
|
29 |
26 28
|
mulcld |
|
30 |
29
|
sincld |
|
31 |
|
0red |
|
32 |
|
2re |
|
33 |
32
|
a1i |
|
34 |
|
1red |
|
35 |
33 34
|
remulcld |
|
36 |
35 34
|
resubcld |
|
37 |
25
|
zred |
|
38 |
|
0lt1 |
|
39 |
|
2t1e2 |
|
40 |
39
|
oveq1i |
|
41 |
|
2m1e1 |
|
42 |
40 41
|
eqtr2i |
|
43 |
38 42
|
breqtri |
|
44 |
43
|
a1i |
|
45 |
23
|
zred |
|
46 |
|
nnre |
|
47 |
|
0le2 |
|
48 |
47
|
a1i |
|
49 |
|
nnge1 |
|
50 |
34 46 33 48 49
|
lemul2ad |
|
51 |
35 45 34 50
|
lesub1dd |
|
52 |
31 36 37 44 51
|
ltletrd |
|
53 |
31 52
|
gtned |
|
54 |
30 26 53
|
divcld |
|
55 |
54
|
adantl |
|
56 |
|
picn |
|
57 |
56
|
a1i |
|
58 |
|
4cn |
|
59 |
58
|
a1i |
|
60 |
|
4ne0 |
|
61 |
60
|
a1i |
|
62 |
57 59 61
|
divcld |
|
63 |
|
eqid |
|
64 |
|
0cnd |
|
65 |
58
|
a1i |
|
66 |
|
nncn |
|
67 |
|
mulcl |
|
68 |
66 56 67
|
sylancl |
|
69 |
56
|
a1i |
|
70 |
|
nnne0 |
|
71 |
|
0re |
|
72 |
|
pipos |
|
73 |
71 72
|
gtneii |
|
74 |
73
|
a1i |
|
75 |
66 69 70 74
|
mulne0d |
|
76 |
65 68 75
|
divcld |
|
77 |
27
|
a1i |
|
78 |
66 77
|
mulcld |
|
79 |
78
|
sincld |
|
80 |
76 79
|
mulcld |
|
81 |
64 80
|
ifcld |
|
82 |
63 81
|
fmpti |
|
83 |
82
|
a1i |
|
84 |
|
eqidd |
|
85 |
|
breq2 |
|
86 |
|
oveq1 |
|
87 |
86
|
oveq2d |
|
88 |
|
oveq1 |
|
89 |
88
|
fveq2d |
|
90 |
87 89
|
oveq12d |
|
91 |
85 90
|
ifbieq2d |
|
92 |
91
|
adantl |
|
93 |
|
c0ex |
|
94 |
|
ovex |
|
95 |
93 94
|
ifex |
|
96 |
95
|
a1i |
|
97 |
84 92 15 96
|
fvmptd |
|
98 |
97
|
adantr |
|
99 |
|
simpr |
|
100 |
|
simpl |
|
101 |
|
2nn |
|
102 |
|
nndivdvds |
|
103 |
100 101 102
|
sylancl |
|
104 |
99 103
|
mpbird |
|
105 |
104
|
iftrued |
|
106 |
98 105
|
eqtrd |
|
107 |
106
|
3adant1 |
|
108 |
|
1re |
|
109 |
108
|
renegcli |
|
110 |
108 109
|
ifcli |
|
111 |
110
|
a1i |
|
112 |
2 111
|
fmpti |
|
113 |
|
oveq1 |
|
114 |
113
|
breq1d |
|
115 |
114
|
ifbid |
|
116 |
115
|
cbvmptv |
|
117 |
2 116
|
eqtri |
|
118 |
117
|
a1i |
|
119 |
|
oveq1 |
|
120 |
|
pire |
|
121 |
32 120
|
remulcli |
|
122 |
1 121
|
eqeltri |
|
123 |
122
|
recni |
|
124 |
123
|
mulid2i |
|
125 |
124
|
eqcomi |
|
126 |
125
|
oveq2i |
|
127 |
126
|
oveq1i |
|
128 |
119 127
|
eqtrdi |
|
129 |
128
|
adantl |
|
130 |
|
simpl |
|
131 |
|
2pos |
|
132 |
32 120 131 72
|
mulgt0ii |
|
133 |
1
|
eqcomi |
|
134 |
132 133
|
breqtri |
|
135 |
122 134
|
elrpii |
|
136 |
135
|
a1i |
|
137 |
|
1zzd |
|
138 |
|
modcyc |
|
139 |
130 136 137 138
|
syl3anc |
|
140 |
129 139
|
eqtrd |
|
141 |
140
|
breq1d |
|
142 |
141
|
ifbid |
|
143 |
|
id |
|
144 |
122
|
a1i |
|
145 |
143 144
|
readdcld |
|
146 |
118 142 145 111
|
fvmptd |
|
147 |
2
|
fvmpt2 |
|
148 |
110 147
|
mpan2 |
|
149 |
146 148
|
eqtr4d |
|
150 |
|
eqid |
|
151 |
|
snfi |
|
152 |
|
eldifi |
|
153 |
|
0xr |
|
154 |
153
|
a1i |
|
155 |
120
|
rexri |
|
156 |
155
|
a1i |
|
157 |
|
elioore |
|
158 |
157
|
adantr |
|
159 |
|
simpr |
|
160 |
120
|
renegcli |
|
161 |
160
|
rexri |
|
162 |
|
iooltub |
|
163 |
161 155 162
|
mp3an12 |
|
164 |
163
|
adantr |
|
165 |
154 156 158 159 164
|
eliood |
|
166 |
|
negpilt0 |
|
167 |
160 71 166
|
ltleii |
|
168 |
|
iooss1 |
|
169 |
161 167 168
|
mp2an |
|
170 |
169
|
sseli |
|
171 |
2
|
reseq1i |
|
172 |
|
ioossre |
|
173 |
|
resmpt |
|
174 |
172 173
|
ax-mp |
|
175 |
|
elioore |
|
176 |
135
|
a1i |
|
177 |
|
0red |
|
178 |
|
ioogtlb |
|
179 |
153 155 178
|
mp3an12 |
|
180 |
177 175 179
|
ltled |
|
181 |
120
|
a1i |
|
182 |
122
|
a1i |
|
183 |
170 163
|
syl |
|
184 |
|
pirp |
|
185 |
|
2timesgt |
|
186 |
184 185
|
ax-mp |
|
187 |
186 133
|
breqtri |
|
188 |
187
|
a1i |
|
189 |
175 181 182 183 188
|
lttrd |
|
190 |
|
modid |
|
191 |
175 176 180 189 190
|
syl22anc |
|
192 |
191 183
|
eqbrtrd |
|
193 |
192
|
iftrued |
|
194 |
193
|
mpteq2ia |
|
195 |
171 174 194
|
3eqtrri |
|
196 |
195
|
oveq2i |
|
197 |
|
reelprrecn |
|
198 |
197
|
a1i |
|
199 |
|
iooretop |
|
200 |
|
eqid |
|
201 |
200
|
tgioo2 |
|
202 |
199 201
|
eleqtri |
|
203 |
202
|
a1i |
|
204 |
|
1cnd |
|
205 |
198 203 204
|
dvmptconst |
|
206 |
205
|
mptru |
|
207 |
|
ssid |
|
208 |
|
ax-resscn |
|
209 |
|
fss |
|
210 |
112 208 209
|
mp2an |
|
211 |
|
dvresioo |
|
212 |
207 210 211
|
mp2an |
|
213 |
196 206 212
|
3eqtr3i |
|
214 |
213
|
dmeqi |
|
215 |
|
eqid |
|
216 |
93 215
|
dmmpti |
|
217 |
214 216
|
eqtr3i |
|
218 |
|
ssdmres |
|
219 |
217 218
|
mpbir |
|
220 |
219
|
sseli |
|
221 |
170 220
|
elind |
|
222 |
|
dmres |
|
223 |
221 222
|
eleqtrrdi |
|
224 |
165 223
|
syl |
|
225 |
224
|
adantlr |
|
226 |
161
|
a1i |
|
227 |
153
|
a1i |
|
228 |
157
|
ad2antrr |
|
229 |
|
ioogtlb |
|
230 |
161 155 229
|
mp3an12 |
|
231 |
230
|
ad2antrr |
|
232 |
|
0red |
|
233 |
|
neqne |
|
234 |
233
|
ad2antlr |
|
235 |
|
simpr |
|
236 |
228 232 234 235
|
lttri5d |
|
237 |
226 227 228 231 236
|
eliood |
|
238 |
71 120 72
|
ltleii |
|
239 |
|
iooss2 |
|
240 |
155 238 239
|
mp2an |
|
241 |
240
|
sseli |
|
242 |
2
|
reseq1i |
|
243 |
|
ioossre |
|
244 |
|
resmpt |
|
245 |
243 244
|
ax-mp |
|
246 |
120
|
a1i |
|
247 |
|
elioore |
|
248 |
135
|
a1i |
|
249 |
247 248
|
modcld |
|
250 |
247 145
|
syl |
|
251 |
56
|
2timesi |
|
252 |
1 251
|
eqtri |
|
253 |
252
|
oveq2i |
|
254 |
|
negpicn |
|
255 |
254 56 56
|
addassi |
|
256 |
255
|
eqcomi |
|
257 |
56
|
negidi |
|
258 |
56 254 257
|
addcomli |
|
259 |
258
|
oveq1i |
|
260 |
56
|
addid2i |
|
261 |
259 260
|
eqtri |
|
262 |
253 256 261
|
3eqtrri |
|
263 |
262
|
a1i |
|
264 |
160
|
a1i |
|
265 |
122
|
a1i |
|
266 |
241 230
|
syl |
|
267 |
264 247 265 266
|
ltadd1dd |
|
268 |
263 267
|
eqbrtrd |
|
269 |
246 250 268
|
ltled |
|
270 |
|
0red |
|
271 |
160 122
|
readdcli |
|
272 |
271
|
a1i |
|
273 |
72
|
a1i |
|
274 |
273 262
|
breqtrdi |
|
275 |
270 272 250 274 267
|
lttrd |
|
276 |
270 250 275
|
ltled |
|
277 |
247
|
recnd |
|
278 |
123
|
a1i |
|
279 |
277 278
|
addcomd |
|
280 |
|
iooltub |
|
281 |
161 153 280
|
mp3an12 |
|
282 |
|
ltaddneg |
|
283 |
247 122 282
|
sylancl |
|
284 |
281 283
|
mpbid |
|
285 |
279 284
|
eqbrtrd |
|
286 |
276 285
|
jca |
|
287 |
|
modid2 |
|
288 |
250 135 287
|
sylancl |
|
289 |
286 288
|
mpbird |
|
290 |
127
|
a1i |
|
291 |
135
|
a1i |
|
292 |
|
1zzd |
|
293 |
143 291 292 138
|
syl3anc |
|
294 |
290 293
|
eqtrd |
|
295 |
247 294
|
syl |
|
296 |
289 295
|
eqtr3d |
|
297 |
269 296
|
breqtrd |
|
298 |
246 249 297
|
lensymd |
|
299 |
298
|
iffalsed |
|
300 |
299
|
mpteq2ia |
|
301 |
242 245 300
|
3eqtrri |
|
302 |
301
|
oveq2i |
|
303 |
|
iooretop |
|
304 |
303 201
|
eleqtri |
|
305 |
304
|
a1i |
|
306 |
204
|
negcld |
|
307 |
198 305 306
|
dvmptconst |
|
308 |
307
|
mptru |
|
309 |
|
dvresioo |
|
310 |
207 210 309
|
mp2an |
|
311 |
302 308 310
|
3eqtr3i |
|
312 |
311
|
dmeqi |
|
313 |
|
eqid |
|
314 |
93 313
|
dmmpti |
|
315 |
312 314
|
eqtr3i |
|
316 |
|
ssdmres |
|
317 |
315 316
|
mpbir |
|
318 |
317
|
sseli |
|
319 |
241 318
|
elind |
|
320 |
319 222
|
eleqtrrdi |
|
321 |
237 320
|
syl |
|
322 |
225 321
|
pm2.61dan |
|
323 |
152 322
|
sylan |
|
324 |
|
eldifn |
|
325 |
324
|
adantr |
|
326 |
323 325
|
condan |
|
327 |
|
velsn |
|
328 |
326 327
|
sylibr |
|
329 |
328
|
ssriv |
|
330 |
|
ssfi |
|
331 |
151 329 330
|
mp2an |
|
332 |
|
inss1 |
|
333 |
222 332
|
eqsstri |
|
334 |
|
ioosscn |
|
335 |
333 334
|
sstri |
|
336 |
335
|
a1i |
|
337 |
|
dvf |
|
338 |
|
fresin |
|
339 |
|
ffdm |
|
340 |
337 338 339
|
mp2b |
|
341 |
340
|
simpli |
|
342 |
341
|
a1i |
|
343 |
161
|
a1i |
|
344 |
153
|
a1i |
|
345 |
|
ioossre |
|
346 |
333
|
sseli |
|
347 |
345 346
|
sseldi |
|
348 |
347
|
adantr |
|
349 |
346 230
|
syl |
|
350 |
349
|
adantr |
|
351 |
|
simpr |
|
352 |
343 344 348 350 351
|
eliood |
|
353 |
|
elun1 |
|
354 |
352 353
|
syl |
|
355 |
|
simpl |
|
356 |
|
0red |
|
357 |
347
|
adantr |
|
358 |
|
simpr |
|
359 |
356 357 358
|
nltled |
|
360 |
|
id |
|
361 |
207
|
a1i |
|
362 |
|
eqid |
|
363 |
210
|
a1i |
|
364 |
|
0red |
|
365 |
|
mnfxr |
|
366 |
365
|
a1i |
|
367 |
364
|
mnfltd |
|
368 |
362 366 364 367
|
lptioo2 |
|
369 |
|
incom |
|
370 |
|
ioossre |
|
371 |
|
df-ss |
|
372 |
370 371
|
mpbi |
|
373 |
369 372
|
eqtr2i |
|
374 |
373
|
fveq2i |
|
375 |
368 374
|
eleqtrdi |
|
376 |
|
pnfxr |
|
377 |
376
|
a1i |
|
378 |
364
|
ltpnfd |
|
379 |
362 364 377 378
|
lptioo1 |
|
380 |
|
incom |
|
381 |
|
ioossre |
|
382 |
|
df-ss |
|
383 |
381 382
|
mpbi |
|
384 |
380 383
|
eqtr2i |
|
385 |
384
|
fveq2i |
|
386 |
379 385
|
eleqtrdi |
|
387 |
|
eqid |
|
388 |
|
mnfle |
|
389 |
161 388
|
ax-mp |
|
390 |
|
iooss1 |
|
391 |
365 389 390
|
mp2an |
|
392 |
391
|
a1i |
|
393 |
|
ioosscn |
|
394 |
392 393
|
sstrdi |
|
395 |
|
0cnd |
|
396 |
387 394 306 395
|
constlimc |
|
397 |
|
resabs1 |
|
398 |
391 397
|
ax-mp |
|
399 |
301 398
|
eqtr4i |
|
400 |
399
|
oveq1i |
|
401 |
|
fssres |
|
402 |
210 370 401
|
mp2an |
|
403 |
402
|
a1i |
|
404 |
393
|
a1i |
|
405 |
|
eqid |
|
406 |
|
0le0 |
|
407 |
|
elioc2 |
|
408 |
161 71 407
|
mp2an |
|
409 |
71 166 406 408
|
mpbir3an |
|
410 |
200
|
cnfldtop |
|
411 |
|
ovex |
|
412 |
|
resttop |
|
413 |
410 411 412
|
mp2an |
|
414 |
161
|
a1i |
|
415 |
|
eqid |
|
416 |
389
|
a1i |
|
417 |
366 414 364 362 415 416 364
|
iocopn |
|
418 |
417
|
mptru |
|
419 |
201
|
oveq1i |
|
420 |
|
iocssre |
|
421 |
365 71 420
|
mp2an |
|
422 |
197
|
elexi |
|
423 |
|
restabs |
|
424 |
410 421 422 423
|
mp3an |
|
425 |
419 424
|
eqtri |
|
426 |
418 425
|
eleqtri |
|
427 |
|
isopn3i |
|
428 |
413 426 427
|
mp2an |
|
429 |
|
mnflt0 |
|
430 |
|
ioounsn |
|
431 |
365 153 429 430
|
mp3an |
|
432 |
431
|
eqcomi |
|
433 |
432
|
oveq2i |
|
434 |
433
|
fveq2i |
|
435 |
|
ioounsn |
|
436 |
161 153 166 435
|
mp3an |
|
437 |
436
|
eqcomi |
|
438 |
434 437
|
fveq12i |
|
439 |
428 438
|
eqtr3i |
|
440 |
409 439
|
eleqtri |
|
441 |
440
|
a1i |
|
442 |
403 392 404 200 405 441
|
limcres |
|
443 |
442
|
mptru |
|
444 |
400 443
|
eqtri |
|
445 |
396 444
|
eleqtrdi |
|
446 |
|
eqid |
|
447 |
|
ioosscn |
|
448 |
447
|
a1i |
|
449 |
446 448 204 395
|
constlimc |
|
450 |
|
ltpnf |
|
451 |
|
xrltle |
|
452 |
155 376 451
|
mp2an |
|
453 |
120 450 452
|
mp2b |
|
454 |
|
iooss2 |
|
455 |
376 453 454
|
mp2an |
|
456 |
|
resabs1 |
|
457 |
455 456
|
ax-mp |
|
458 |
195 457
|
eqtr4i |
|
459 |
458
|
oveq1i |
|
460 |
|
fssres |
|
461 |
210 381 460
|
mp2an |
|
462 |
461
|
a1i |
|
463 |
455
|
a1i |
|
464 |
|
ioosscn |
|
465 |
464
|
a1i |
|
466 |
|
eqid |
|
467 |
|
elico2 |
|
468 |
71 155 467
|
mp2an |
|
469 |
71 406 72 468
|
mpbir3an |
|
470 |
|
ovex |
|
471 |
|
resttop |
|
472 |
410 470 471
|
mp2an |
|
473 |
155
|
a1i |
|
474 |
|
eqid |
|
475 |
453
|
a1i |
|
476 |
364 473 377 362 474 475
|
icoopn |
|
477 |
476
|
mptru |
|
478 |
201
|
oveq1i |
|
479 |
|
rge0ssre |
|
480 |
|
restabs |
|
481 |
410 479 422 480
|
mp3an |
|
482 |
478 481
|
eqtri |
|
483 |
477 482
|
eleqtri |
|
484 |
|
isopn3i |
|
485 |
472 483 484
|
mp2an |
|
486 |
|
0ltpnf |
|
487 |
|
snunioo1 |
|
488 |
153 376 486 487
|
mp3an |
|
489 |
488
|
eqcomi |
|
490 |
489
|
oveq2i |
|
491 |
490
|
fveq2i |
|
492 |
|
snunioo1 |
|
493 |
153 155 72 492
|
mp3an |
|
494 |
493
|
eqcomi |
|
495 |
491 494
|
fveq12i |
|
496 |
485 495
|
eqtr3i |
|
497 |
469 496
|
eleqtri |
|
498 |
497
|
a1i |
|
499 |
462 463 465 200 466 498
|
limcres |
|
500 |
499
|
mptru |
|
501 |
459 500
|
eqtri |
|
502 |
449 501
|
eleqtrdi |
|
503 |
|
neg1lt0 |
|
504 |
109 71 108
|
lttri |
|
505 |
503 38 504
|
mp2an |
|
506 |
109 505
|
ltneii |
|
507 |
506
|
a1i |
|
508 |
200 361 362 363 364 375 386 445 502 507
|
jumpncnp |
|
509 |
508
|
mptru |
|
510 |
208
|
a1i |
|
511 |
210
|
a1i |
|
512 |
207
|
a1i |
|
513 |
|
inss2 |
|
514 |
222 513
|
eqsstri |
|
515 |
514
|
sseli |
|
516 |
201 200
|
dvcnp2 |
|
517 |
510 511 512 515 516
|
syl31anc |
|
518 |
509 517
|
mto |
|
519 |
518
|
a1i |
|
520 |
360 519
|
eqneltrd |
|
521 |
520
|
necon2ai |
|
522 |
521
|
adantr |
|
523 |
356 357 359 522
|
leneltd |
|
524 |
346 165
|
sylan |
|
525 |
|
elun2 |
|
526 |
524 525
|
syl |
|
527 |
355 523 526
|
syl2anc |
|
528 |
354 527
|
pm2.61dan |
|
529 |
|
ovex |
|
530 |
|
ovex |
|
531 |
529 530
|
unipr |
|
532 |
528 531
|
eleqtrrdi |
|
533 |
532
|
ssriv |
|
534 |
533
|
a1i |
|
535 |
|
ineq2 |
|
536 |
|
retop |
|
537 |
|
ovex |
|
538 |
537
|
resex |
|
539 |
538
|
dmex |
|
540 |
536 539
|
pm3.2i |
|
541 |
320
|
ssriv |
|
542 |
|
ssid |
|
543 |
303 541 542
|
3pm3.2i |
|
544 |
|
restopnb |
|
545 |
540 543 544
|
mp2an |
|
546 |
303 545
|
mpbi |
|
547 |
|
inss2 |
|
548 |
541 542
|
ssini |
|
549 |
547 548
|
eqssi |
|
550 |
201
|
oveq1i |
|
551 |
333 345
|
sstri |
|
552 |
|
restabs |
|
553 |
410 551 422 552
|
mp3an |
|
554 |
550 553
|
eqtr2i |
|
555 |
546 549 554
|
3eltr4i |
|
556 |
535 555
|
eqeltrdi |
|
557 |
556
|
adantl |
|
558 |
|
neqne |
|
559 |
|
elprn1 |
|
560 |
558 559
|
sylan2 |
|
561 |
|
ineq2 |
|
562 |
223
|
ssriv |
|
563 |
|
ssid |
|
564 |
199 562 563
|
3pm3.2i |
|
565 |
|
restopnb |
|
566 |
540 564 565
|
mp2an |
|
567 |
199 566
|
mpbi |
|
568 |
|
inss2 |
|
569 |
562 563
|
ssini |
|
570 |
568 569
|
eqssi |
|
571 |
567 570 554
|
3eltr4i |
|
572 |
561 571
|
eqeltrdi |
|
573 |
560 572
|
syl |
|
574 |
557 573
|
pm2.61dan |
|
575 |
574
|
adantl |
|
576 |
|
ssid |
|
577 |
576
|
a1i |
|
578 |
394 395 577
|
constcncfg |
|
579 |
578
|
mptru |
|
580 |
579
|
a1i |
|
581 |
|
reseq2 |
|
582 |
|
resabs1 |
|
583 |
240 582
|
ax-mp |
|
584 |
583 311
|
eqtr4i |
|
585 |
581 584
|
eqtrdi |
|
586 |
535 549
|
eqtrdi |
|
587 |
586
|
oveq1d |
|
588 |
580 585 587
|
3eltr4d |
|
589 |
588
|
adantl |
|
590 |
448 395 577
|
constcncfg |
|
591 |
590
|
mptru |
|
592 |
591
|
a1i |
|
593 |
|
reseq2 |
|
594 |
|
resabs1 |
|
595 |
169 594
|
ax-mp |
|
596 |
595 213
|
eqtr4i |
|
597 |
593 596
|
eqtrdi |
|
598 |
561 570
|
eqtrdi |
|
599 |
598
|
oveq1d |
|
600 |
592 597 599
|
3eltr4d |
|
601 |
560 600
|
syl |
|
602 |
589 601
|
pm2.61dan |
|
603 |
602
|
adantl |
|
604 |
336 342 534 575 603
|
cncfuni |
|
605 |
604
|
mptru |
|
606 |
|
oveq1 |
|
607 |
606
|
reseq2d |
|
608 |
|
iooss2 |
|
609 |
376 453 608
|
mp2an |
|
610 |
|
resabs2 |
|
611 |
609 610
|
ax-mp |
|
612 |
607 611
|
eqtrdi |
|
613 |
|
id |
|
614 |
612 613
|
oveq12d |
|
615 |
254
|
a1i |
|
616 |
313 394 395 615
|
constlimc |
|
617 |
616
|
mptru |
|
618 |
311
|
oveq1i |
|
619 |
337
|
a1i |
|
620 |
160
|
a1i |
|
621 |
153
|
a1i |
|
622 |
166
|
a1i |
|
623 |
317
|
a1i |
|
624 |
238
|
a1i |
|
625 |
619 620 621 622 623 473 624
|
limcresioolb |
|
626 |
625
|
mptru |
|
627 |
618 626
|
eqtri |
|
628 |
617 627
|
eleqtri |
|
629 |
628
|
ne0ii |
|
630 |
629
|
a1i |
|
631 |
614 630
|
eqnetrd |
|
632 |
631
|
adantl |
|
633 |
|
eldifi |
|
634 |
161
|
a1i |
|
635 |
155
|
a1i |
|
636 |
|
icossre |
|
637 |
160 155 636
|
mp2an |
|
638 |
637
|
sseli |
|
639 |
638
|
adantr |
|
640 |
160
|
a1i |
|
641 |
|
icogelb |
|
642 |
161 155 641
|
mp3an12 |
|
643 |
642
|
adantr |
|
644 |
|
neqne |
|
645 |
644
|
adantl |
|
646 |
640 639 643 645
|
leneltd |
|
647 |
|
icoltub |
|
648 |
161 155 647
|
mp3an12 |
|
649 |
648
|
adantr |
|
650 |
634 635 639 646 649
|
eliood |
|
651 |
633 650
|
sylan |
|
652 |
|
eldifn |
|
653 |
652
|
adantr |
|
654 |
651 653
|
eldifd |
|
655 |
|
oveq1 |
|
656 |
655
|
reseq2d |
|
657 |
656 360
|
oveq12d |
|
658 |
215 448 395 395
|
constlimc |
|
659 |
658
|
mptru |
|
660 |
|
resres |
|
661 |
|
iooin |
|
662 |
161 155 153 376 661
|
mp4an |
|
663 |
167
|
iftruei |
|
664 |
453
|
iftruei |
|
665 |
663 664
|
oveq12i |
|
666 |
662 665
|
eqtri |
|
667 |
666
|
reseq2i |
|
668 |
213
|
eqcomi |
|
669 |
660 667 668
|
3eqtrri |
|
670 |
669
|
oveq1i |
|
671 |
659 670
|
eleqtri |
|
672 |
671
|
ne0ii |
|
673 |
672
|
a1i |
|
674 |
657 673
|
eqnetrd |
|
675 |
654 326 674
|
3syl |
|
676 |
632 675
|
pm2.61dan |
|
677 |
|
oveq2 |
|
678 |
677
|
reseq2d |
|
679 |
|
id |
|
680 |
678 679
|
oveq12d |
|
681 |
|
iooss1 |
|
682 |
365 389 681
|
mp2an |
|
683 |
|
resabs2 |
|
684 |
682 683
|
ax-mp |
|
685 |
684
|
oveq1i |
|
686 |
680 685
|
eqtrdi |
|
687 |
215 448 395 57
|
constlimc |
|
688 |
687
|
mptru |
|
689 |
213
|
oveq1i |
|
690 |
120
|
a1i |
|
691 |
72
|
a1i |
|
692 |
219
|
a1i |
|
693 |
167
|
a1i |
|
694 |
619 621 690 691 692 414 693
|
limcresiooub |
|
695 |
694
|
mptru |
|
696 |
689 695
|
eqtri |
|
697 |
688 696
|
eleqtri |
|
698 |
697
|
ne0ii |
|
699 |
698
|
a1i |
|
700 |
686 699
|
eqnetrd |
|
701 |
700
|
adantl |
|
702 |
161
|
a1i |
|
703 |
155
|
a1i |
|
704 |
|
negpitopissre |
|
705 |
|
eldifi |
|
706 |
704 705
|
sseldi |
|
707 |
706
|
adantr |
|
708 |
161
|
a1i |
|
709 |
155
|
a1i |
|
710 |
|
iocgtlb |
|
711 |
708 709 705 710
|
syl3anc |
|
712 |
711
|
adantr |
|
713 |
120
|
a1i |
|
714 |
|
iocleub |
|
715 |
708 709 705 714
|
syl3anc |
|
716 |
715
|
adantr |
|
717 |
|
id |
|
718 |
717
|
eqcomd |
|
719 |
718
|
necon3bi |
|
720 |
719
|
adantl |
|
721 |
707 713 716 720
|
leneltd |
|
722 |
702 703 707 712 721
|
eliood |
|
723 |
|
eldifn |
|
724 |
723
|
adantr |
|
725 |
722 724
|
eldifd |
|
726 |
|
oveq2 |
|
727 |
726
|
reseq2d |
|
728 |
727 360
|
oveq12d |
|
729 |
313 394 395 395
|
constlimc |
|
730 |
729
|
mptru |
|
731 |
|
resres |
|
732 |
|
iooin |
|
733 |
161 155 365 153 732
|
mp4an |
|
734 |
|
mnflt |
|
735 |
160 734
|
ax-mp |
|
736 |
|
xrltnle |
|
737 |
365 161 736
|
mp2an |
|
738 |
735 737
|
mpbi |
|
739 |
738
|
iffalsei |
|
740 |
|
xrltnle |
|
741 |
153 155 740
|
mp2an |
|
742 |
72 741
|
mpbi |
|
743 |
742
|
iffalsei |
|
744 |
739 743
|
oveq12i |
|
745 |
733 744
|
eqtri |
|
746 |
745
|
reseq2i |
|
747 |
311
|
eqcomi |
|
748 |
731 746 747
|
3eqtrri |
|
749 |
748
|
oveq1i |
|
750 |
730 749
|
eleqtri |
|
751 |
750
|
ne0ii |
|
752 |
751
|
a1i |
|
753 |
728 752
|
eqnetrd |
|
754 |
725 326 753
|
3syl |
|
755 |
701 754
|
pm2.61dan |
|
756 |
|
eqid |
|
757 |
|
ioosscn |
|
758 |
757
|
a1i |
|
759 |
|
1cnd |
|
760 |
27
|
a1i |
|
761 |
756 758 759 760
|
constlimc |
|
762 |
|
ioossioc |
|
763 |
762
|
sseli |
|
764 |
763
|
iftrued |
|
765 |
210
|
a1i |
|
766 |
|
modcl |
|
767 |
3 135 766
|
mp2an |
|
768 |
3 767
|
resubcli |
|
769 |
768
|
rexri |
|
770 |
769
|
a1i |
|
771 |
3
|
a1i |
|
772 |
|
elioore |
|
773 |
|
ioogtlb |
|
774 |
153 155 773
|
mp3an12 |
|
775 |
772 774
|
elrpd |
|
776 |
771 775
|
ltsubrpd |
|
777 |
|
ioossre |
|
778 |
777
|
a1i |
|
779 |
365
|
a1i |
|
780 |
|
mnflt |
|
781 |
|
xrltle |
|
782 |
365 769 781
|
mp2an |
|
783 |
768 780 782
|
mp2b |
|
784 |
783
|
a1i |
|
785 |
765 770 771 776 778 779 784
|
limcresiooub |
|
786 |
|
iooltub |
|
787 |
153 155 786
|
mp3an12 |
|
788 |
210
|
a1i |
|
789 |
777
|
a1i |
|
790 |
788 789
|
feqresmpt |
|
791 |
|
elioore |
|
792 |
791 110 147
|
sylancl |
|
793 |
792
|
adantl |
|
794 |
791
|
adantl |
|
795 |
135
|
a1i |
|
796 |
794 795
|
modcld |
|
797 |
767
|
a1i |
|
798 |
120
|
a1i |
|
799 |
3
|
a1i |
|
800 |
135
|
a1i |
|
801 |
|
ioossico |
|
802 |
801
|
sseli |
|
803 |
799 800 802
|
ltmod |
|
804 |
803
|
adantl |
|
805 |
|
simpl |
|
806 |
796 797 798 804 805
|
lttrd |
|
807 |
806
|
iftrued |
|
808 |
793 807
|
eqtrd |
|
809 |
808
|
mpteq2dva |
|
810 |
790 809
|
eqtrd |
|
811 |
787 810
|
syl |
|
812 |
811
|
oveq1d |
|
813 |
785 812
|
eqtr3d |
|
814 |
761 764 813
|
3eltr4d |
|
815 |
|
eqid |
|
816 |
|
ioossre |
|
817 |
816
|
a1i |
|
818 |
817 208
|
sstrdi |
|
819 |
27
|
a1i |
|
820 |
815 818 306 819
|
constlimc |
|
821 |
820
|
mptru |
|
822 |
821
|
a1i |
|
823 |
|
id |
|
824 |
|
lbioc |
|
825 |
824
|
a1i |
|
826 |
823 825
|
eqneltrd |
|
827 |
826
|
iffalsed |
|
828 |
210
|
a1i |
|
829 |
816
|
a1i |
|
830 |
828 829
|
feqresmpt |
|
831 |
829
|
sselda |
|
832 |
831 110 147
|
sylancl |
|
833 |
120
|
a1i |
|
834 |
135
|
a1i |
|
835 |
831 834
|
modcld |
|
836 |
3 120
|
resubcli |
|
837 |
836
|
a1i |
|
838 |
122
|
a1i |
|
839 |
837 838
|
readdcld |
|
840 |
|
elioore |
|
841 |
840 838
|
readdcld |
|
842 |
3
|
a1i |
|
843 |
836
|
rexri |
|
844 |
843
|
a1i |
|
845 |
842
|
rexrd |
|
846 |
|
id |
|
847 |
|
ioogtlb |
|
848 |
844 845 846 847
|
syl3anc |
|
849 |
837 840 838 848
|
ltadd1dd |
|
850 |
839 841 842 849
|
ltsub1dd |
|
851 |
850
|
adantl |
|
852 |
252
|
oveq2i |
|
853 |
56 56
|
addcli |
|
854 |
|
subadd23 |
|
855 |
27 56 853 854
|
mp3an |
|
856 |
56 56
|
pncan3oi |
|
857 |
856
|
oveq2i |
|
858 |
852 855 857
|
3eqtri |
|
859 |
858
|
oveq1i |
|
860 |
|
pncan2 |
|
861 |
27 56 860
|
mp2an |
|
862 |
859 861
|
eqtr2i |
|
863 |
862
|
a1i |
|
864 |
841 842
|
resubcld |
|
865 |
|
modabs2 |
|
866 |
864 135 865
|
sylancl |
|
867 |
135
|
a1i |
|
868 |
|
0red |
|
869 |
839 842
|
resubcld |
|
870 |
72 862
|
breqtri |
|
871 |
870
|
a1i |
|
872 |
868 869 864 871 850
|
lttrd |
|
873 |
868 864 872
|
ltled |
|
874 |
842 838
|
readdcld |
|
875 |
|
iooltub |
|
876 |
844 845 846 875
|
syl3anc |
|
877 |
840 842 838 876
|
ltadd1dd |
|
878 |
841 874 842 877
|
ltsub1dd |
|
879 |
|
pncan2 |
|
880 |
27 123 879
|
mp2an |
|
881 |
878 880
|
breqtrdi |
|
882 |
|
modid |
|
883 |
864 867 873 881 882
|
syl22anc |
|
884 |
866 883
|
eqtr2d |
|
885 |
884
|
adantl |
|
886 |
|
oveq2 |
|
887 |
886
|
adantr |
|
888 |
864 867
|
modcld |
|
889 |
888
|
recnd |
|
890 |
889
|
addid1d |
|
891 |
890
|
adantl |
|
892 |
887 891
|
eqtr2d |
|
893 |
892
|
oveq1d |
|
894 |
|
modaddabs |
|
895 |
864 842 867 894
|
syl3anc |
|
896 |
895
|
adantl |
|
897 |
885 893 896
|
3eqtrd |
|
898 |
145
|
recnd |
|
899 |
27
|
a1i |
|
900 |
898 899
|
npcand |
|
901 |
124
|
a1i |
|
902 |
901
|
oveq2d |
|
903 |
900 902
|
eqtr4d |
|
904 |
903
|
oveq1d |
|
905 |
840 904
|
syl |
|
906 |
905
|
adantl |
|
907 |
|
1zzd |
|
908 |
831 834 907 138
|
syl3anc |
|
909 |
897 906 908
|
3eqtrrd |
|
910 |
851 863 909
|
3brtr4d |
|
911 |
833 835 910
|
ltled |
|
912 |
833 835 911
|
lensymd |
|
913 |
912
|
iffalsed |
|
914 |
832 913
|
eqtrd |
|
915 |
914
|
mpteq2dva |
|
916 |
830 915
|
eqtr2d |
|
917 |
916
|
oveq1d |
|
918 |
843
|
a1i |
|
919 |
3
|
a1i |
|
920 |
|
ltsubrp |
|
921 |
3 184 920
|
mp2an |
|
922 |
921
|
a1i |
|
923 |
|
mnflt |
|
924 |
|
xrltle |
|
925 |
365 843 924
|
mp2an |
|
926 |
836 923 925
|
mp2b |
|
927 |
926
|
a1i |
|
928 |
363 918 919 922 817 366 927
|
limcresiooub |
|
929 |
928
|
mptru |
|
930 |
917 929
|
eqtr2di |
|
931 |
822 827 930
|
3eltr4d |
|
932 |
931
|
adantl |
|
933 |
155
|
a1i |
|
934 |
122
|
rexri |
|
935 |
934
|
a1i |
|
936 |
767
|
rexri |
|
937 |
936
|
a1i |
|
938 |
120
|
a1i |
|
939 |
767
|
a1i |
|
940 |
|
pm4.56 |
|
941 |
940
|
biimpi |
|
942 |
|
olc |
|
943 |
942
|
adantl |
|
944 |
153
|
a1i |
|
945 |
155
|
a1i |
|
946 |
767
|
a1i |
|
947 |
|
0red |
|
948 |
767
|
a1i |
|
949 |
|
modge0 |
|
950 |
3 135 949
|
mp2an |
|
951 |
950
|
a1i |
|
952 |
|
id |
|
953 |
947 948 951 952
|
leneltd |
|
954 |
953
|
adantl |
|
955 |
|
simpl |
|
956 |
944 945 946 954 955
|
eliood |
|
957 |
956
|
orcd |
|
958 |
943 957
|
pm2.61dane |
|
959 |
941 958
|
nsyl |
|
960 |
938 939 959
|
nltled |
|
961 |
|
modlt |
|
962 |
3 135 961
|
mp2an |
|
963 |
962
|
a1i |
|
964 |
933 935 937 960 963
|
elicod |
|
965 |
|
eqid |
|
966 |
965 818 204 819
|
constlimc |
|
967 |
966
|
mptru |
|
968 |
967
|
a1i |
|
969 |
|
id |
|
970 |
|
ubioc1 |
|
971 |
153 155 72 970
|
mp3an |
|
972 |
969 971
|
eqeltrdi |
|
973 |
972
|
iftrued |
|
974 |
363 817
|
feqresmpt |
|
975 |
974
|
mptru |
|
976 |
840 110 147
|
sylancl |
|
977 |
976
|
adantl |
|
978 |
|
simpr |
|
979 |
969
|
eqcomd |
|
980 |
979
|
oveq2d |
|
981 |
980
|
oveq1d |
|
982 |
981
|
adantr |
|
983 |
978 982
|
eleqtrd |
|
984 |
983 803
|
syl |
|
985 |
|
simpl |
|
986 |
984 985
|
breqtrd |
|
987 |
986
|
iftrued |
|
988 |
977 987
|
eqtrd |
|
989 |
988
|
mpteq2dva |
|
990 |
975 989
|
eqtr2id |
|
991 |
990
|
oveq1d |
|
992 |
991 929
|
eqtr2di |
|
993 |
968 973 992
|
3eltr4d |
|
994 |
993
|
adantl |
|
995 |
155
|
a1i |
|
996 |
934
|
a1i |
|
997 |
767
|
a1i |
|
998 |
120
|
a1i |
|
999 |
|
icogelb |
|
1000 |
155 934 999
|
mp3an12 |
|
1001 |
1000
|
adantr |
|
1002 |
|
neqne |
|
1003 |
1002
|
adantl |
|
1004 |
998 997 1001 1003
|
leneltd |
|
1005 |
962
|
a1i |
|
1006 |
995 996 997 1004 1005
|
eliood |
|
1007 |
|
eqid |
|
1008 |
|
ioossre |
|
1009 |
1008
|
a1i |
|
1010 |
1009 208
|
sstrdi |
|
1011 |
|
neg1cn |
|
1012 |
1011
|
a1i |
|
1013 |
27
|
a1i |
|
1014 |
1007 1010 1012 1013
|
constlimc |
|
1015 |
153
|
a1i |
|
1016 |
120
|
a1i |
|
1017 |
936
|
a1i |
|
1018 |
|
ioogtlb |
|
1019 |
155 934 1018
|
mp3an12 |
|
1020 |
1015 1016 1017 1019
|
gtnelioc |
|
1021 |
1020
|
iffalsed |
|
1022 |
1008
|
a1i |
|
1023 |
363 1022
|
feqresmpt |
|
1024 |
1023
|
mptru |
|
1025 |
|
elioore |
|
1026 |
1025 110 147
|
sylancl |
|
1027 |
1026
|
adantl |
|
1028 |
120
|
a1i |
|
1029 |
135
|
a1i |
|
1030 |
1025 1029
|
modcld |
|
1031 |
1030
|
adantl |
|
1032 |
3 120
|
readdcli |
|
1033 |
1032
|
recni |
|
1034 |
1033
|
a1i |
|
1035 |
27
|
a1i |
|
1036 |
767
|
recni |
|
1037 |
1036
|
a1i |
|
1038 |
1034 1035 1037
|
nnncan2d |
|
1039 |
1038 861
|
eqtr2di |
|
1040 |
1032 767
|
resubcli |
|
1041 |
1040
|
a1i |
|
1042 |
768
|
a1i |
|
1043 |
1040
|
rexri |
|
1044 |
1043
|
a1i |
|
1045 |
3
|
a1i |
|
1046 |
1045
|
rexrd |
|
1047 |
|
id |
|
1048 |
|
ioogtlb |
|
1049 |
1044 1046 1047 1048
|
syl3anc |
|
1050 |
1041 1025 1042 1049
|
ltsub1dd |
|
1051 |
1039 1050
|
eqbrtrd |
|
1052 |
1025
|
recnd |
|
1053 |
|
sub31 |
|
1054 |
1052 1035 1037 1053
|
syl3anc |
|
1055 |
1051 1054
|
breqtrd |
|
1056 |
1055
|
adantl |
|
1057 |
1045 1025
|
resubcld |
|
1058 |
|
0red |
|
1059 |
|
iooltub |
|
1060 |
1044 1046 1047 1059
|
syl3anc |
|
1061 |
1025 1045
|
posdifd |
|
1062 |
1060 1061
|
mpbid |
|
1063 |
1058 1057 1062
|
ltled |
|
1064 |
1045 1041
|
resubcld |
|
1065 |
122
|
a1i |
|
1066 |
1041 1025 1045 1049
|
ltsub2dd |
|
1067 |
|
sub31 |
|
1068 |
27 1033 1036 1067
|
mp3an |
|
1069 |
861
|
oveq2i |
|
1070 |
1068 1069
|
eqtri |
|
1071 |
|
ltsubrp |
|
1072 |
767 184 1071
|
mp2an |
|
1073 |
767 120
|
resubcli |
|
1074 |
1073 767 122
|
lttri |
|
1075 |
1072 962 1074
|
mp2an |
|
1076 |
1070 1075
|
eqbrtri |
|
1077 |
1076
|
a1i |
|
1078 |
1057 1064 1065 1066 1077
|
lttrd |
|
1079 |
|
modid |
|
1080 |
1057 1029 1063 1078 1079
|
syl22anc |
|
1081 |
1080
|
oveq2d |
|
1082 |
1081
|
oveq1d |
|
1083 |
767
|
a1i |
|
1084 |
1083 1057
|
resubcld |
|
1085 |
120
|
a1i |
|
1086 |
1054 1084
|
eqeltrd |
|
1087 |
72
|
a1i |
|
1088 |
1058 1085 1086 1087 1051
|
lttrd |
|
1089 |
1088 1054
|
breqtrd |
|
1090 |
1058 1084 1089
|
ltled |
|
1091 |
1045 1042
|
resubcld |
|
1092 |
1025 1045 1042 1060
|
ltsub1dd |
|
1093 |
|
nncan |
|
1094 |
27 1036 1093
|
mp2an |
|
1095 |
1094 962
|
eqbrtri |
|
1096 |
1095
|
a1i |
|
1097 |
1086 1091 1065 1092 1096
|
lttrd |
|
1098 |
1054 1097
|
eqbrtrrd |
|
1099 |
|
modid |
|
1100 |
1084 1029 1090 1098 1099
|
syl22anc |
|
1101 |
1082 1100
|
eqtr2d |
|
1102 |
|
modsubmodmod |
|
1103 |
1045 1057 1029 1102
|
syl3anc |
|
1104 |
1035 1052
|
nncand |
|
1105 |
1104
|
oveq1d |
|
1106 |
1101 1103 1105
|
3eqtrd |
|
1107 |
1106
|
adantl |
|
1108 |
1056 1107
|
breqtrd |
|
1109 |
1019 1108
|
sylan |
|
1110 |
1028 1031 1109
|
ltled |
|
1111 |
1028 1031 1110
|
lensymd |
|
1112 |
1111
|
iffalsed |
|
1113 |
1027 1112
|
eqtrd |
|
1114 |
1113
|
mpteq2dva |
|
1115 |
1024 1114
|
eqtr2id |
|
1116 |
1115
|
oveq1d |
|
1117 |
210
|
a1i |
|
1118 |
1043
|
a1i |
|
1119 |
3
|
a1i |
|
1120 |
|
elioore |
|
1121 |
|
ltaddsublt |
|
1122 |
1119 1016 1120 1121
|
syl3anc |
|
1123 |
1019 1122
|
mpbid |
|
1124 |
365
|
a1i |
|
1125 |
|
mnflt |
|
1126 |
|
xrltle |
|
1127 |
365 1043 1126
|
mp2an |
|
1128 |
1040 1125 1127
|
mp2b |
|
1129 |
1128
|
a1i |
|
1130 |
1117 1118 1119 1123 1009 1124 1129
|
limcresiooub |
|
1131 |
1116 1130
|
eqtr2d |
|
1132 |
1014 1021 1131
|
3eltr4d |
|
1133 |
1006 1132
|
syl |
|
1134 |
994 1133
|
pm2.61dan |
|
1135 |
964 1134
|
syl |
|
1136 |
932 1135
|
pm2.61dan |
|
1137 |
814 1136
|
pm2.61i |
|
1138 |
|
eqid |
|
1139 |
|
ioossre |
|
1140 |
1139
|
a1i |
|
1141 |
1140 208
|
sstrdi |
|
1142 |
1138 1141 204 819
|
constlimc |
|
1143 |
1142
|
mptru |
|
1144 |
1143
|
a1i |
|
1145 |
2
|
a1i |
|
1146 |
|
oveq1 |
|
1147 |
1146
|
breq1d |
|
1148 |
1147
|
ifbid |
|
1149 |
1148
|
adantl |
|
1150 |
3
|
a1i |
|
1151 |
108 109
|
ifcli |
|
1152 |
1151
|
a1i |
|
1153 |
1145 1149 1150 1152
|
fvmptd |
|
1154 |
|
icoltub |
|
1155 |
153 155 1154
|
mp3an12 |
|
1156 |
1155
|
iftrued |
|
1157 |
1153 1156
|
eqtrd |
|
1158 |
363 1140
|
feqresmpt |
|
1159 |
1158
|
mptru |
|
1160 |
|
elioore |
|
1161 |
1160 110 147
|
sylancl |
|
1162 |
1161
|
adantl |
|
1163 |
3
|
a1i |
|
1164 |
1160 1163
|
resubcld |
|
1165 |
135
|
a1i |
|
1166 |
|
0red |
|
1167 |
1163
|
rexrd |
|
1168 |
120 767
|
resubcli |
|
1169 |
3 1168
|
readdcli |
|
1170 |
1169
|
rexri |
|
1171 |
1170
|
a1i |
|
1172 |
|
id |
|
1173 |
|
ioogtlb |
|
1174 |
1167 1171 1172 1173
|
syl3anc |
|
1175 |
1163 1160
|
posdifd |
|
1176 |
1174 1175
|
mpbid |
|
1177 |
1166 1164 1176
|
ltled |
|
1178 |
120
|
a1i |
|
1179 |
122
|
a1i |
|
1180 |
1169
|
a1i |
|
1181 |
1180 1163
|
resubcld |
|
1182 |
|
iooltub |
|
1183 |
1167 1171 1172 1182
|
syl3anc |
|
1184 |
1160 1180 1163 1183
|
ltsub1dd |
|
1185 |
1168
|
recni |
|
1186 |
|
pncan2 |
|
1187 |
27 1185 1186
|
mp2an |
|
1188 |
|
subge02 |
|
1189 |
120 767 1188
|
mp2an |
|
1190 |
950 1189
|
mpbi |
|
1191 |
1187 1190
|
eqbrtri |
|
1192 |
1191
|
a1i |
|
1193 |
1164 1181 1178 1184 1192
|
ltletrd |
|
1194 |
187
|
a1i |
|
1195 |
1164 1178 1179 1193 1194
|
lttrd |
|
1196 |
|
modid |
|
1197 |
1164 1165 1177 1195 1196
|
syl22anc |
|
1198 |
1197
|
oveq2d |
|
1199 |
1198
|
oveq1d |
|
1200 |
767
|
a1i |
|
1201 |
1200 1164
|
readdcld |
|
1202 |
1163 1163
|
resubcld |
|
1203 |
1200 1202
|
readdcld |
|
1204 |
27
|
subidi |
|
1205 |
1204
|
oveq2i |
|
1206 |
1036
|
addid1i |
|
1207 |
1205 1206
|
eqtr2i |
|
1208 |
950 1207
|
breqtri |
|
1209 |
1208
|
a1i |
|
1210 |
1163 1160 1163 1174
|
ltsub1dd |
|
1211 |
1202 1164 1200 1210
|
ltadd2dd |
|
1212 |
1166 1203 1201 1209 1211
|
lelttrd |
|
1213 |
1166 1201 1212
|
ltled |
|
1214 |
1164 1181 1200 1184
|
ltadd2dd |
|
1215 |
1187
|
oveq2i |
|
1216 |
1036 56
|
pncan3i |
|
1217 |
1215 1216
|
eqtri |
|
1218 |
1214 1217
|
breqtrdi |
|
1219 |
1201 1178 1179 1218 1194
|
lttrd |
|
1220 |
|
modid |
|
1221 |
1201 1165 1213 1219 1220
|
syl22anc |
|
1222 |
1199 1221
|
eqtr2d |
|
1223 |
|
modaddabs |
|
1224 |
1163 1164 1165 1223
|
syl3anc |
|
1225 |
27
|
a1i |
|
1226 |
1160
|
recnd |
|
1227 |
1225 1226
|
pncan3d |
|
1228 |
1227
|
oveq1d |
|
1229 |
1222 1224 1228
|
3eqtrrd |
|
1230 |
1229
|
adantl |
|
1231 |
1218
|
adantl |
|
1232 |
1230 1231
|
eqbrtrd |
|
1233 |
1155 1232
|
sylan |
|
1234 |
1233
|
iftrued |
|
1235 |
1162 1234
|
eqtrd |
|
1236 |
1235
|
mpteq2dva |
|
1237 |
1159 1236
|
eqtr2id |
|
1238 |
1237
|
oveq1d |
|
1239 |
210
|
a1i |
|
1240 |
1170
|
a1i |
|
1241 |
1168
|
a1i |
|
1242 |
767
|
a1i |
|
1243 |
120
|
a1i |
|
1244 |
1242 1243
|
posdifd |
|
1245 |
1155 1244
|
mpbid |
|
1246 |
1241 1245
|
elrpd |
|
1247 |
1150 1246
|
ltaddrpd |
|
1248 |
1139
|
a1i |
|
1249 |
376
|
a1i |
|
1250 |
|
ltpnf |
|
1251 |
|
xrltle |
|
1252 |
1170 376 1251
|
mp2an |
|
1253 |
1169 1250 1252
|
mp2b |
|
1254 |
1253
|
a1i |
|
1255 |
1239 1150 1240 1247 1248 1249 1254
|
limcresioolb |
|
1256 |
1238 1255
|
eqtr2d |
|
1257 |
1144 1157 1256
|
3eltr4d |
|
1258 |
155
|
a1i |
|
1259 |
934
|
a1i |
|
1260 |
936
|
a1i |
|
1261 |
153
|
a1i |
|
1262 |
155
|
a1i |
|
1263 |
936
|
a1i |
|
1264 |
950
|
a1i |
|
1265 |
767
|
a1i |
|
1266 |
120
|
a1i |
|
1267 |
1265 1266
|
ltnled |
|
1268 |
1267
|
ibir |
|
1269 |
1268
|
adantl |
|
1270 |
1261 1262 1263 1264 1269
|
elicod |
|
1271 |
|
simpl |
|
1272 |
1270 1271
|
condan |
|
1273 |
962
|
a1i |
|
1274 |
1258 1259 1260 1272 1273
|
elicod |
|
1275 |
|
eqid |
|
1276 |
|
ioossre |
|
1277 |
1276
|
a1i |
|
1278 |
1277 208
|
sstrdi |
|
1279 |
1275 1278 306 819
|
constlimc |
|
1280 |
1279
|
mptru |
|
1281 |
1280
|
a1i |
|
1282 |
|
1ex |
|
1283 |
109
|
elexi |
|
1284 |
1282 1283
|
ifex |
|
1285 |
1148 2 1284
|
fvmpt |
|
1286 |
3 1285
|
ax-mp |
|
1287 |
1286
|
a1i |
|
1288 |
120
|
a1i |
|
1289 |
767
|
a1i |
|
1290 |
1288 1289 1000
|
lensymd |
|
1291 |
1290
|
iffalsed |
|
1292 |
1287 1291
|
eqtrd |
|
1293 |
363 1277
|
feqresmpt |
|
1294 |
1293
|
mptru |
|
1295 |
|
elioore |
|
1296 |
1295 110 147
|
sylancl |
|
1297 |
1296
|
adantl |
|
1298 |
120
|
a1i |
|
1299 |
3
|
a1i |
|
1300 |
1295 1299
|
resubcld |
|
1301 |
135
|
a1i |
|
1302 |
|
0red |
|
1303 |
1299
|
rexrd |
|
1304 |
122 767
|
resubcli |
|
1305 |
3 1304
|
readdcli |
|
1306 |
1305
|
rexri |
|
1307 |
1306
|
a1i |
|
1308 |
|
id |
|
1309 |
|
ioogtlb |
|
1310 |
1303 1307 1308 1309
|
syl3anc |
|
1311 |
1299 1295
|
posdifd |
|
1312 |
1310 1311
|
mpbid |
|
1313 |
1302 1300 1312
|
ltled |
|
1314 |
1305
|
a1i |
|
1315 |
1314 1299
|
resubcld |
|
1316 |
122
|
a1i |
|
1317 |
|
iooltub |
|
1318 |
1303 1307 1308 1317
|
syl3anc |
|
1319 |
1295 1314 1299 1318
|
ltsub1dd |
|
1320 |
1304
|
recni |
|
1321 |
|
pncan2 |
|
1322 |
27 1320 1321
|
mp2an |
|
1323 |
|
subge02 |
|
1324 |
122 767 1323
|
mp2an |
|
1325 |
950 1324
|
mpbi |
|
1326 |
1322 1325
|
eqbrtri |
|
1327 |
1326
|
a1i |
|
1328 |
1300 1315 1316 1319 1327
|
ltletrd |
|
1329 |
1300 1301 1313 1328 1196
|
syl22anc |
|
1330 |
1329
|
oveq2d |
|
1331 |
1330
|
oveq1d |
|
1332 |
|
readdcl |
|
1333 |
767 1300 1332
|
sylancr |
|
1334 |
767
|
a1i |
|
1335 |
950
|
a1i |
|
1336 |
1334 1300 1335 1312
|
addgegt0d |
|
1337 |
1302 1333 1336
|
ltled |
|
1338 |
1300 1315 1334 1319
|
ltadd2dd |
|
1339 |
1322
|
oveq2i |
|
1340 |
1036 123
|
pncan3i |
|
1341 |
1339 1340
|
eqtri |
|
1342 |
1338 1341
|
breqtrdi |
|
1343 |
1333 1301 1337 1342 1220
|
syl22anc |
|
1344 |
1331 1343
|
eqtr2d |
|
1345 |
1299 1300 1301 1223
|
syl3anc |
|
1346 |
27
|
a1i |
|
1347 |
1295
|
recnd |
|
1348 |
1346 1347
|
pncan3d |
|
1349 |
1348
|
oveq1d |
|
1350 |
1344 1345 1349
|
3eqtrd |
|
1351 |
1350
|
adantl |
|
1352 |
1333
|
adantl |
|
1353 |
1351 1352
|
eqeltrrd |
|
1354 |
767
|
a1i |
|
1355 |
1000
|
adantr |
|
1356 |
1300 1312
|
elrpd |
|
1357 |
1334 1356
|
ltaddrpd |
|
1358 |
1357
|
adantl |
|
1359 |
1298 1354 1352 1355 1358
|
lelttrd |
|
1360 |
1298 1352 1359
|
ltled |
|
1361 |
1360 1351
|
breqtrd |
|
1362 |
1298 1353 1361
|
lensymd |
|
1363 |
1362
|
iffalsed |
|
1364 |
1297 1363
|
eqtrd |
|
1365 |
1364
|
mpteq2dva |
|
1366 |
1294 1365
|
eqtr2id |
|
1367 |
1366
|
oveq1d |
|
1368 |
210
|
a1i |
|
1369 |
3
|
a1i |
|
1370 |
1306
|
a1i |
|
1371 |
1304
|
a1i |
|
1372 |
962
|
a1i |
|
1373 |
122
|
a1i |
|
1374 |
1289 1373
|
posdifd |
|
1375 |
1372 1374
|
mpbid |
|
1376 |
1371 1375
|
elrpd |
|
1377 |
1369 1376
|
ltaddrpd |
|
1378 |
1276
|
a1i |
|
1379 |
376
|
a1i |
|
1380 |
|
ltpnf |
|
1381 |
|
xrltle |
|
1382 |
1306 376 1381
|
mp2an |
|
1383 |
1305 1380 1382
|
mp2b |
|
1384 |
1383
|
a1i |
|
1385 |
1368 1369 1370 1377 1378 1379 1384
|
limcresioolb |
|
1386 |
1367 1385
|
eqtr2d |
|
1387 |
1281 1292 1386
|
3eltr4d |
|
1388 |
1274 1387
|
syl |
|
1389 |
1257 1388
|
pm2.61i |
|
1390 |
|
id |
|
1391 |
1 2 1390
|
sqwvfoura |
|
1392 |
1391
|
eqcomd |
|
1393 |
1392
|
mpteq2ia |
|
1394 |
|
id |
|
1395 |
1 2 1394
|
sqwvfourb |
|
1396 |
1395
|
eqcomd |
|
1397 |
1396
|
mpteq2ia |
|
1398 |
|
nnnn0 |
|
1399 |
|
0red |
|
1400 |
|
eqid |
|
1401 |
1400
|
fvmpt2 |
|
1402 |
1398 1399 1401
|
syl2anc |
|
1403 |
1402
|
oveq1d |
|
1404 |
78
|
coscld |
|
1405 |
1404
|
mul02d |
|
1406 |
1403 1405
|
eqtrd |
|
1407 |
|
ovex |
|
1408 |
93 1407
|
ifex |
|
1409 |
|
eqid |
|
1410 |
1409
|
fvmpt2 |
|
1411 |
1408 1410
|
mpan2 |
|
1412 |
1411
|
oveq1d |
|
1413 |
1406 1412
|
oveq12d |
|
1414 |
64 76
|
ifcld |
|
1415 |
1414 79
|
mulcld |
|
1416 |
1415
|
addid2d |
|
1417 |
|
iftrue |
|
1418 |
1417
|
oveq1d |
|
1419 |
79
|
mul02d |
|
1420 |
1418 1419
|
sylan9eqr |
|
1421 |
|
iftrue |
|
1422 |
1421
|
eqcomd |
|
1423 |
1422
|
adantl |
|
1424 |
1420 1423
|
eqtrd |
|
1425 |
|
iffalse |
|
1426 |
1425
|
oveq1d |
|
1427 |
1426
|
adantl |
|
1428 |
|
iffalse |
|
1429 |
1428
|
eqcomd |
|
1430 |
1429
|
adantl |
|
1431 |
1427 1430
|
eqtrd |
|
1432 |
1424 1431
|
pm2.61dan |
|
1433 |
1413 1416 1432
|
3eqtrrd |
|
1434 |
1433
|
mpteq2ia |
|
1435 |
112 1 149 150 331 605 676 755 3 1137 1389 1393 1397 1434
|
fourierclim |
|
1436 |
|
0nn0 |
|
1437 |
|
eqidd |
|
1438 |
1437 1400 93
|
fvmpt |
|
1439 |
1436 1438
|
ax-mp |
|
1440 |
1439
|
oveq1i |
|
1441 |
32
|
recni |
|
1442 |
71 131
|
gtneii |
|
1443 |
1441 1442
|
div0i |
|
1444 |
1440 1443
|
eqtri |
|
1445 |
1444
|
oveq2i |
|
1446 |
204
|
mptru |
|
1447 |
1446 1011
|
ifcli |
|
1448 |
1151
|
recni |
|
1449 |
1286 1448
|
eqeltri |
|
1450 |
1447 1449
|
addcli |
|
1451 |
1450 1441 1442
|
divcli |
|
1452 |
1451
|
subid1i |
|
1453 |
1445 1452
|
eqtri |
|
1454 |
1435 1453
|
breqtri |
|
1455 |
1454
|
a1i |
|
1456 |
83 107 1455
|
sumnnodd |
|
1457 |
1456
|
mptru |
|
1458 |
1457
|
simpli |
|
1459 |
|
breq2 |
|
1460 |
|
oveq1 |
|
1461 |
1460
|
oveq2d |
|
1462 |
|
oveq1 |
|
1463 |
1462
|
fveq2d |
|
1464 |
1461 1463
|
oveq12d |
|
1465 |
1459 1464
|
ifbieq2d |
|
1466 |
1465
|
adantl |
|
1467 |
|
elnnz |
|
1468 |
25 52 1467
|
sylanbrc |
|
1469 |
|
ovex |
|
1470 |
93 1469
|
ifex |
|
1471 |
1470
|
a1i |
|
1472 |
84 1466 1468 1471
|
fvmptd |
|
1473 |
|
dvdsmul1 |
|
1474 |
20 22 1473
|
sylancr |
|
1475 |
23
|
zcnd |
|
1476 |
|
1cnd |
|
1477 |
1475 1476
|
npcand |
|
1478 |
1477
|
eqcomd |
|
1479 |
1474 1478
|
breqtrd |
|
1480 |
|
oddp1even |
|
1481 |
25 1480
|
syl |
|
1482 |
1479 1481
|
mpbird |
|
1483 |
1482
|
iffalsed |
|
1484 |
56
|
a1i |
|
1485 |
26 1484
|
mulcomd |
|
1486 |
1485
|
oveq2d |
|
1487 |
58
|
a1i |
|
1488 |
73
|
a1i |
|
1489 |
1487 1484 26 1488 53
|
divdiv1d |
|
1490 |
1486 1489
|
eqtr4d |
|
1491 |
1490
|
oveq1d |
|
1492 |
1487 1484 1488
|
divcld |
|
1493 |
1492 26 30 53
|
div32d |
|
1494 |
1491 1493
|
eqtrd |
|
1495 |
1472 1483 1494
|
3eqtrd |
|
1496 |
1495
|
mpteq2ia |
|
1497 |
|
oveq2 |
|
1498 |
1497
|
oveq1d |
|
1499 |
1498
|
oveq1d |
|
1500 |
1499
|
fveq2d |
|
1501 |
1500 1498
|
oveq12d |
|
1502 |
1501
|
oveq2d |
|
1503 |
1502
|
cbvmptv |
|
1504 |
1496 1503
|
eqtri |
|
1505 |
|
seqeq3 |
|
1506 |
1504 1505
|
ax-mp |
|
1507 |
1 2 3 5
|
fourierswlem |
|
1508 |
1507
|
eqcomi |
|
1509 |
1458 1506 1508
|
3brtr3i |
|
1510 |
1509
|
a1i |
|
1511 |
|
eqid |
|
1512 |
65 69 74
|
divcld |
|
1513 |
1441
|
a1i |
|
1514 |
1513 66
|
mulcld |
|
1515 |
|
id |
|
1516 |
|
1cnd |
|
1517 |
1515 1516
|
subcld |
|
1518 |
1514 1517
|
syl |
|
1519 |
1518 77
|
mulcld |
|
1520 |
1519
|
sincld |
|
1521 |
32
|
a1i |
|
1522 |
|
nnre |
|
1523 |
1521 1522
|
remulcld |
|
1524 |
1523
|
recnd |
|
1525 |
|
1cnd |
|
1526 |
1524 1525
|
subcld |
|
1527 |
|
1red |
|
1528 |
39 1521
|
eqeltrid |
|
1529 |
|
1lt2 |
|
1530 |
1529
|
a1i |
|
1531 |
1530 39
|
breqtrrdi |
|
1532 |
47
|
a1i |
|
1533 |
|
nnge1 |
|
1534 |
1527 1522 1521 1532 1533
|
lemul2ad |
|
1535 |
1527 1528 1523 1531 1534
|
ltletrd |
|
1536 |
1527 1535
|
gtned |
|
1537 |
1524 1525 1536
|
subne0d |
|
1538 |
1520 1526 1537
|
divcld |
|
1539 |
1512 1538
|
mulcld |
|
1540 |
1511 1539
|
fmpti |
|
1541 |
1540
|
a1i |
|
1542 |
1541
|
ffvelrnda |
|
1543 |
|
divcan6 |
|
1544 |
56 73 58 60 1543
|
mp4an |
|
1545 |
1544
|
eqcomi |
|
1546 |
1545
|
oveq1i |
|
1547 |
54
|
mulid2d |
|
1548 |
60
|
a1i |
|
1549 |
1484 1487 1548
|
divcld |
|
1550 |
1549 1492 54
|
mulassd |
|
1551 |
1546 1547 1550
|
3eqtr3a |
|
1552 |
|
eqidd |
|
1553 |
13
|
oveq2d |
|
1554 |
1553
|
adantl |
|
1555 |
1494 1469
|
eqeltrrdi |
|
1556 |
1552 1554 15 1555
|
fvmptd |
|
1557 |
1556
|
oveq2d |
|
1558 |
1557
|
eqcomd |
|
1559 |
18 1551 1558
|
3eqtrd |
|
1560 |
1559
|
adantl |
|
1561 |
6 7 62 1510 1542 1560
|
isermulc2 |
|
1562 |
|
climrel |
|
1563 |
1562
|
releldmi |
|
1564 |
1561 1563
|
syl |
|
1565 |
6 7 19 55 1564
|
isumclim2 |
|
1566 |
1565
|
mptru |
|
1567 |
1561
|
mptru |
|
1568 |
|
climuni |
|
1569 |
1566 1567 1568
|
mp2an |
|
1570 |
1569
|
oveq2i |
|
1571 |
58 56 73
|
divcli |
|
1572 |
56 58 60
|
divcli |
|
1573 |
1286 1151
|
eqeltri |
|
1574 |
71 1573
|
ifcli |
|
1575 |
5 1574
|
eqeltri |
|
1576 |
1575
|
recni |
|
1577 |
1571 1572 1576
|
mulassi |
|
1578 |
1572 1571 1544
|
mulcomli |
|
1579 |
1578
|
oveq1i |
|
1580 |
1576
|
mulid2i |
|
1581 |
1579 1580
|
eqtri |
|
1582 |
1570 1577 1581
|
3eqtr2i |
|
1583 |
|
seqeq3 |
|
1584 |
4 1583
|
ax-mp |
|
1585 |
1584 1567
|
eqbrtri |
|
1586 |
1582 1585
|
pm3.2i |
|