Step |
Hyp |
Ref |
Expression |
1 |
|
psdmul.s |
|
2 |
|
psdmul.b |
|
3 |
|
psdmul.p |
|
4 |
|
psdmul.m |
|
5 |
|
psdmul.r |
|
6 |
|
psdmul.x |
|
7 |
|
psdmul.f |
|
8 |
|
psdmul.g |
|
9 |
|
eqid |
|
10 |
|
eqid |
|
11 |
5
|
crngringd |
|
12 |
11
|
ringcmnd |
|
13 |
12
|
adantr |
|
14 |
|
simpr |
|
15 |
|
reldmpsr |
|
16 |
1 2 15
|
strov2rcl |
|
17 |
7 16
|
syl |
|
18 |
|
eqid |
|
19 |
18
|
psrbagsn |
|
20 |
17 19
|
syl |
|
21 |
20
|
adantr |
|
22 |
18
|
psrbagaddcl |
|
23 |
14 21 22
|
syl2anc |
|
24 |
18
|
psrbaglefi |
|
25 |
23 24
|
syl |
|
26 |
|
eqid |
|
27 |
5
|
crnggrpd |
|
28 |
27
|
grpmndd |
|
29 |
28
|
ad2antrr |
|
30 |
18
|
psrbagf |
|
31 |
30
|
adantl |
|
32 |
6
|
adantr |
|
33 |
31 32
|
ffvelcdmd |
|
34 |
|
peano2nn0 |
|
35 |
33 34
|
syl |
|
36 |
35
|
adantr |
|
37 |
|
eqid |
|
38 |
11
|
ad2antrr |
|
39 |
1 9 18 2 7
|
psrelbas |
|
40 |
39
|
ad2antrr |
|
41 |
|
elrabi |
|
42 |
41
|
adantl |
|
43 |
40 42
|
ffvelcdmd |
|
44 |
1 9 18 2 8
|
psrelbas |
|
45 |
44
|
ad2antrr |
|
46 |
|
eqid |
|
47 |
18 46
|
psrbagconcl |
|
48 |
23 47
|
sylan |
|
49 |
|
elrabi |
|
50 |
48 49
|
syl |
|
51 |
45 50
|
ffvelcdmd |
|
52 |
9 37 38 43 51
|
ringcld |
|
53 |
9 26 29 36 52
|
mulgnn0cld |
|
54 |
|
disjdifr |
|
55 |
54
|
a1i |
|
56 |
|
1nn0 |
|
57 |
|
0nn0 |
|
58 |
56 57
|
ifcli |
|
59 |
58
|
nn0ge0i |
|
60 |
31
|
ffvelcdmda |
|
61 |
60
|
nn0red |
|
62 |
58
|
nn0rei |
|
63 |
62
|
a1i |
|
64 |
61 63
|
addge01d |
|
65 |
59 64
|
mpbii |
|
66 |
65
|
ralrimiva |
|
67 |
31
|
ffnd |
|
68 |
56 57
|
ifcli |
|
69 |
68
|
elexi |
|
70 |
|
eqid |
|
71 |
69 70
|
fnmpti |
|
72 |
71
|
a1i |
|
73 |
17
|
adantr |
|
74 |
|
inidm |
|
75 |
67 72 73 73 74
|
offn |
|
76 |
|
eqidd |
|
77 |
|
eqeq1 |
|
78 |
77
|
ifbid |
|
79 |
58
|
elexi |
|
80 |
78 70 79
|
fvmpt |
|
81 |
80
|
adantl |
|
82 |
67 72 73 73 74 76 81
|
ofval |
|
83 |
67 75 73 73 74 76 82
|
ofrfval |
|
84 |
66 83
|
mpbird |
|
85 |
84
|
adantr |
|
86 |
17
|
ad2antrr |
|
87 |
18
|
psrbagf |
|
88 |
87
|
adantl |
|
89 |
31
|
adantr |
|
90 |
18
|
psrbagf |
|
91 |
23 90
|
syl |
|
92 |
91
|
adantr |
|
93 |
|
nn0re |
|
94 |
|
nn0re |
|
95 |
|
nn0re |
|
96 |
|
letr |
|
97 |
93 94 95 96
|
syl3an |
|
98 |
97
|
adantl |
|
99 |
86 88 89 92 98
|
caoftrn |
|
100 |
85 99
|
mpan2d |
|
101 |
100
|
ss2rabdv |
|
102 |
|
undifr |
|
103 |
101 102
|
sylib |
|
104 |
103
|
eqcomd |
|
105 |
9 10 13 25 53 55 104
|
gsummptfidmsplit |
|
106 |
|
eqid |
|
107 |
|
ovex |
|
108 |
107
|
rabex |
|
109 |
108
|
rabex |
|
110 |
109
|
a1i |
|
111 |
|
ovex |
|
112 |
|
eqid |
|
113 |
111 112
|
fnmpti |
|
114 |
113
|
a1i |
|
115 |
|
fvexd |
|
116 |
114 25 115
|
fndmfifsupp |
|
117 |
9 106 26 110 52 116 13 35
|
gsummulg |
|
118 |
|
difrab |
|
119 |
118
|
eleq2i |
|
120 |
|
breq1 |
|
121 |
|
breq1 |
|
122 |
121
|
notbid |
|
123 |
120 122
|
anbi12d |
|
124 |
123
|
elrab |
|
125 |
18
|
psrbagf |
|
126 |
125
|
ffnd |
|
127 |
126
|
adantl |
|
128 |
75
|
adantr |
|
129 |
17
|
ad2antrr |
|
130 |
|
eqidd |
|
131 |
67
|
adantr |
|
132 |
68
|
a1i |
|
133 |
70 132
|
fmpti |
|
134 |
133
|
a1i |
|
135 |
134
|
ffnd |
|
136 |
135
|
ad2antrr |
|
137 |
|
eqidd |
|
138 |
80
|
adantl |
|
139 |
131 136 129 129 74 137 138
|
ofval |
|
140 |
127 128 129 129 74 130 139
|
ofrfval |
|
141 |
127 131 129 129 74 130 137
|
ofrfval |
|
142 |
141
|
notbid |
|
143 |
|
rexnal |
|
144 |
142 143
|
bitr4di |
|
145 |
140 144
|
anbi12d |
|
146 |
33
|
ad2antrr |
|
147 |
125
|
adantl |
|
148 |
6
|
adantr |
|
149 |
147 148
|
ffvelcdmd |
|
150 |
149
|
adantlr |
|
151 |
150
|
adantr |
|
152 |
|
nn0nlt0 |
|
153 |
146 152
|
syl |
|
154 |
31
|
adantr |
|
155 |
154
|
ffvelcdmda |
|
156 |
155
|
nn0cnd |
|
157 |
156
|
addridd |
|
158 |
157
|
breq2d |
|
159 |
158
|
biimpd |
|
160 |
|
ifnefalse |
|
161 |
160
|
oveq2d |
|
162 |
161
|
breq2d |
|
163 |
162
|
imbi1d |
|
164 |
159 163
|
syl5ibrcom |
|
165 |
164
|
imp |
|
166 |
165
|
impancom |
|
167 |
166
|
necon1bd |
|
168 |
167
|
ancrd |
|
169 |
168
|
ex |
|
170 |
169
|
ralimdva |
|
171 |
170
|
anim1d |
|
172 |
171
|
imp |
|
173 |
|
rexim |
|
174 |
173
|
imp |
|
175 |
|
fveq2 |
|
176 |
|
fveq2 |
|
177 |
175 176
|
breq12d |
|
178 |
177
|
notbid |
|
179 |
178
|
ceqsrexbv |
|
180 |
179
|
simprbi |
|
181 |
174 180
|
syl |
|
182 |
33
|
adantr |
|
183 |
182
|
nn0red |
|
184 |
150
|
nn0red |
|
185 |
183 184
|
ltnled |
|
186 |
185
|
biimpar |
|
187 |
181 186
|
sylan2 |
|
188 |
172 187
|
syldan |
|
189 |
|
breq2 |
|
190 |
188 189
|
syl5ibcom |
|
191 |
153 190
|
mtod |
|
192 |
191
|
neqned |
|
193 |
|
elnnne0 |
|
194 |
151 192 193
|
sylanbrc |
|
195 |
|
elfzo0 |
|
196 |
146 194 188 195
|
syl3anbrc |
|
197 |
|
fzostep1 |
|
198 |
196 197
|
syl |
|
199 |
151
|
nn0red |
|
200 |
35
|
ad2antrr |
|
201 |
200
|
nn0red |
|
202 |
6
|
ad2antrr |
|
203 |
|
iftrue |
|
204 |
176 203
|
oveq12d |
|
205 |
175 204
|
breq12d |
|
206 |
205
|
rspcv |
|
207 |
202 206
|
syl |
|
208 |
207
|
imp |
|
209 |
208
|
adantrr |
|
210 |
199 201 209
|
lensymd |
|
211 |
210
|
intn3an3d |
|
212 |
|
elfzo0 |
|
213 |
211 212
|
sylnibr |
|
214 |
198 213
|
orcnd |
|
215 |
145 214
|
sylbida |
|
216 |
215
|
anasss |
|
217 |
124 216
|
sylan2b |
|
218 |
119 217
|
sylan2b |
|
219 |
218
|
oveq1d |
|
220 |
219
|
mpteq2dva |
|
221 |
220
|
oveq2d |
|
222 |
18
|
psrbaglefi |
|
223 |
222
|
adantl |
|
224 |
28
|
ad2antrr |
|
225 |
35
|
adantr |
|
226 |
11
|
ad2antrr |
|
227 |
|
elrabi |
|
228 |
39
|
adantr |
|
229 |
228
|
ffvelcdmda |
|
230 |
227 229
|
sylan2 |
|
231 |
44
|
ad2antrr |
|
232 |
31
|
adantr |
|
233 |
232
|
ffvelcdmda |
|
234 |
233
|
nn0cnd |
|
235 |
227 125
|
syl |
|
236 |
235
|
adantl |
|
237 |
236
|
ffvelcdmda |
|
238 |
237
|
nn0cnd |
|
239 |
58
|
nn0cni |
|
240 |
239
|
a1i |
|
241 |
234 238 240
|
subadd23d |
|
242 |
234 240 238
|
addsubassd |
|
243 |
241 242
|
eqtr4d |
|
244 |
243
|
mpteq2dva |
|
245 |
|
eqid |
|
246 |
18 245
|
psrbagconcl |
|
247 |
|
elrabi |
|
248 |
246 247
|
syl |
|
249 |
248
|
adantll |
|
250 |
18
|
psrbagf |
|
251 |
249 250
|
syl |
|
252 |
251
|
ffnd |
|
253 |
71
|
a1i |
|
254 |
17
|
ad2antrr |
|
255 |
232
|
ffnd |
|
256 |
236
|
ffnd |
|
257 |
|
eqidd |
|
258 |
|
eqidd |
|
259 |
255 256 254 254 74 257 258
|
ofval |
|
260 |
80
|
adantl |
|
261 |
252 253 254 254 74 259 260
|
offval |
|
262 |
|
simplr |
|
263 |
20
|
ad2antrr |
|
264 |
262 263 22
|
syl2anc |
|
265 |
264 90
|
syl |
|
266 |
265
|
ffnd |
|
267 |
255 253 254 254 74 257 260
|
ofval |
|
268 |
266 256 254 254 74 267 258
|
offval |
|
269 |
244 261 268
|
3eqtr4d |
|
270 |
18
|
psrbagaddcl |
|
271 |
249 263 270
|
syl2anc |
|
272 |
269 271
|
eqeltrrd |
|
273 |
231 272
|
ffvelcdmd |
|
274 |
9 37 226 230 273
|
ringcld |
|
275 |
9 26 224 225 274
|
mulgnn0cld |
|
276 |
|
disjdifr |
|
277 |
276
|
a1i |
|
278 |
|
simpl |
|
279 |
278
|
a1i |
|
280 |
279
|
ss2rabi |
|
281 |
280
|
a1i |
|
282 |
|
undifr |
|
283 |
281 282
|
sylib |
|
284 |
283
|
eqcomd |
|
285 |
9 10 13 223 275 277 284
|
gsummptfidmsplit |
|
286 |
|
eldifi |
|
287 |
6
|
ad2antrr |
|
288 |
|
eqidd |
|
289 |
|
eqidd |
|
290 |
255 256 254 254 74 288 289
|
ofval |
|
291 |
287 290
|
mpdan |
|
292 |
286 291
|
sylan2 |
|
293 |
292
|
oveq2d |
|
294 |
236 287
|
ffvelcdmd |
|
295 |
286 294
|
sylan2 |
|
296 |
295
|
nn0cnd |
|
297 |
33
|
nn0cnd |
|
298 |
297
|
adantr |
|
299 |
296 298
|
pncan3d |
|
300 |
293 299
|
eqtrd |
|
301 |
300
|
oveq1d |
|
302 |
251 287
|
ffvelcdmd |
|
303 |
286 302
|
sylan2 |
|
304 |
303
|
nn0cnd |
|
305 |
|
1cnd |
|
306 |
296 304 305
|
addassd |
|
307 |
301 306
|
eqtr3d |
|
308 |
307
|
oveq1d |
|
309 |
28
|
ad2antrr |
|
310 |
|
peano2nn0 |
|
311 |
302 310
|
syl |
|
312 |
286 311
|
sylan2 |
|
313 |
286 274
|
sylan2 |
|
314 |
9 26 10
|
mulgnn0dir |
|
315 |
309 295 312 313 314
|
syl13anc |
|
316 |
308 315
|
eqtrd |
|
317 |
316
|
mpteq2dva |
|
318 |
317
|
oveq2d |
|
319 |
|
difssd |
|
320 |
223 319
|
ssfid |
|
321 |
9 26 224 294 274
|
mulgnn0cld |
|
322 |
286 321
|
sylan2 |
|
323 |
9 26 224 311 274
|
mulgnn0cld |
|
324 |
286 323
|
sylan2 |
|
325 |
|
eqid |
|
326 |
|
eqid |
|
327 |
9 10 13 320 322 324 325 326
|
gsummptfidmadd |
|
328 |
318 327
|
eqtrd |
|
329 |
6
|
ad2antrr |
|
330 |
67
|
adantr |
|
331 |
|
elrabi |
|
332 |
331 126
|
syl |
|
333 |
332
|
adantl |
|
334 |
17
|
ad2antrr |
|
335 |
|
eqidd |
|
336 |
|
eqidd |
|
337 |
330 333 334 334 74 335 336
|
ofval |
|
338 |
329 337
|
mpdan |
|
339 |
|
fveq1 |
|
340 |
339
|
eqeq1d |
|
341 |
121 340
|
anbi12d |
|
342 |
341
|
elrab |
|
343 |
342
|
simprbi |
|
344 |
343
|
simprd |
|
345 |
344
|
adantl |
|
346 |
345
|
oveq2d |
|
347 |
33
|
adantr |
|
348 |
347
|
nn0cnd |
|
349 |
348
|
subid1d |
|
350 |
338 346 349
|
3eqtrrd |
|
351 |
350
|
oveq1d |
|
352 |
351
|
oveq1d |
|
353 |
352
|
mpteq2dva |
|
354 |
353
|
oveq2d |
|
355 |
328 354
|
oveq12d |
|
356 |
27
|
adantr |
|
357 |
108
|
rabex |
|
358 |
357
|
difexi |
|
359 |
358
|
a1i |
|
360 |
322
|
fmpttd |
|
361 |
|
ovex |
|
362 |
361 325
|
fnmpti |
|
363 |
362
|
a1i |
|
364 |
363 320 115
|
fndmfifsupp |
|
365 |
9 106 13 359 360 364
|
gsumcl |
|
366 |
324
|
fmpttd |
|
367 |
|
ovex |
|
368 |
367 326
|
fnmpti |
|
369 |
368
|
a1i |
|
370 |
369 320 115
|
fndmfifsupp |
|
371 |
9 106 13 359 366 370
|
gsumcl |
|
372 |
108
|
rabex |
|
373 |
372
|
a1i |
|
374 |
280
|
sseli |
|
375 |
374 323
|
sylan2 |
|
376 |
375
|
fmpttd |
|
377 |
|
eqid |
|
378 |
367 377
|
fnmpti |
|
379 |
378
|
a1i |
|
380 |
223 281
|
ssfid |
|
381 |
379 380 115
|
fndmfifsupp |
|
382 |
9 106 13 373 376 381
|
gsumcl |
|
383 |
9 10 356 365 371 382
|
grpassd |
|
384 |
285 355 383
|
3eqtrd |
|
385 |
221 384
|
oveq12d |
|
386 |
105 117 385
|
3eqtr3d |
|
387 |
7
|
adantr |
|
388 |
8
|
adantr |
|
389 |
1 2 37 4 18 387 388 23
|
psrmulval |
|
390 |
389
|
oveq2d |
|
391 |
109
|
difexi |
|
392 |
391
|
a1i |
|
393 |
|
eldifi |
|
394 |
41 125
|
syl |
|
395 |
394
|
adantl |
|
396 |
6
|
ad2antrr |
|
397 |
395 396
|
ffvelcdmd |
|
398 |
9 26 29 397 52
|
mulgnn0cld |
|
399 |
393 398
|
sylan2 |
|
400 |
399
|
fmpttd |
|
401 |
|
eqid |
|
402 |
361 401
|
fnmpti |
|
403 |
402
|
a1i |
|
404 |
|
difssd |
|
405 |
25 404
|
ssfid |
|
406 |
403 405 115
|
fndmfifsupp |
|
407 |
9 106 13 392 400 406
|
gsumcl |
|
408 |
9 10 356 371 382
|
grpcld |
|
409 |
9 10 356 407 365 408
|
grpassd |
|
410 |
386 390 409
|
3eqtr4d |
|
411 |
410
|
mpteq2dva |
|
412 |
1 2 4 11 7 8
|
psrmulcl |
|
413 |
1 2 18 6 412
|
psdval |
|
414 |
27
|
grpmgmd |
|
415 |
1 2 414 6 7
|
psdcl |
|
416 |
1 2 4 11 415 8
|
psrmulcl |
|
417 |
1 2 414 6 8
|
psdcl |
|
418 |
1 2 4 11 7 417
|
psrmulcl |
|
419 |
1 2 10 3 416 418
|
psradd |
|
420 |
1 9 18 2 416
|
psrelbas |
|
421 |
420
|
ffnd |
|
422 |
1 9 18 2 418
|
psrelbas |
|
423 |
422
|
ffnd |
|
424 |
108
|
a1i |
|
425 |
|
inidm |
|
426 |
415
|
adantr |
|
427 |
1 2 37 4 18 426 388 14
|
psrmulval |
|
428 |
357
|
a1i |
|
429 |
11
|
ad2antrr |
|
430 |
|
elrabi |
|
431 |
1 9 18 2 415
|
psrelbas |
|
432 |
431
|
adantr |
|
433 |
432
|
ffvelcdmda |
|
434 |
430 433
|
sylan2 |
|
435 |
44
|
ad2antrr |
|
436 |
18 245
|
psrbagconcl |
|
437 |
436
|
adantll |
|
438 |
|
elrabi |
|
439 |
437 438
|
syl |
|
440 |
435 439
|
ffvelcdmd |
|
441 |
9 37 429 434 440
|
ringcld |
|
442 |
441
|
fmpttd |
|
443 |
|
ovex |
|
444 |
|
eqid |
|
445 |
443 444
|
fnmpti |
|
446 |
445
|
a1i |
|
447 |
446 223 115
|
fndmfifsupp |
|
448 |
|
eqid |
|
449 |
|
df-of |
|
450 |
|
vex |
|
451 |
450
|
a1i |
|
452 |
|
ssv |
|
453 |
452
|
a1i |
|
454 |
|
ssv |
|
455 |
454
|
a1i |
|
456 |
449 451 453 455
|
elimampo |
|
457 |
456
|
biimpa |
|
458 |
|
elrabi |
|
459 |
18
|
psrbagf |
|
460 |
459
|
ffund |
|
461 |
458 460
|
syl |
|
462 |
461
|
funfnd |
|
463 |
462
|
ad2antrl |
|
464 |
|
velsn |
|
465 |
|
funmpt |
|
466 |
|
funeq |
|
467 |
465 466
|
mpbiri |
|
468 |
467
|
funfnd |
|
469 |
464 468
|
sylbi |
|
470 |
469
|
ad2antll |
|
471 |
|
vex |
|
472 |
471
|
dmex |
|
473 |
472
|
a1i |
|
474 |
|
vex |
|
475 |
474
|
dmex |
|
476 |
475
|
a1i |
|
477 |
|
eqid |
|
478 |
|
eqidd |
|
479 |
|
eqidd |
|
480 |
463 470 473 476 477 478 479
|
offval |
|
481 |
480
|
eqeq2d |
|
482 |
|
elsni |
|
483 |
482
|
oveq2d |
|
484 |
483
|
eqeq2d |
|
485 |
484
|
ad2antll |
|
486 |
17
|
ad3antrrr |
|
487 |
458 459
|
syl |
|
488 |
487
|
adantl |
|
489 |
133
|
a1i |
|
490 |
|
nn0cn |
|
491 |
|
nn0cn |
|
492 |
|
nn0cn |
|
493 |
|
addsubass |
|
494 |
490 491 492 493
|
syl3an |
|
495 |
494
|
adantl |
|
496 |
486 488 489 489 495
|
caofass |
|
497 |
|
simpr |
|
498 |
58
|
a1i |
|
499 |
70 78 497 498
|
fvmptd3 |
|
500 |
135 135 17 17 74 499 499
|
offval |
|
501 |
500
|
oveq2d |
|
502 |
501
|
ad3antrrr |
|
503 |
239
|
subidi |
|
504 |
503
|
mpteq2i |
|
505 |
|
fconstmpt |
|
506 |
504 505
|
eqtr4i |
|
507 |
506
|
oveq2i |
|
508 |
|
0zd |
|
509 |
490
|
addridd |
|
510 |
509
|
adantl |
|
511 |
486 488 508 510
|
caofid0r |
|
512 |
507 511
|
eqtrid |
|
513 |
496 502 512
|
3eqtrd |
|
514 |
|
simpr |
|
515 |
513 514
|
eqeltrd |
|
516 |
|
oveq1 |
|
517 |
516
|
eleq1d |
|
518 |
515 517
|
syl5ibrcom |
|
519 |
518
|
adantrr |
|
520 |
485 519
|
sylbid |
|
521 |
481 520
|
sylbird |
|
522 |
521
|
rexlimdvva |
|
523 |
457 522
|
mpd |
|
524 |
|
simpr |
|
525 |
17
|
mptexd |
|
526 |
|
elsng |
|
527 |
525 526
|
syl |
|
528 |
70 527
|
mpbiri |
|
529 |
528
|
ad2antrr |
|
530 |
449
|
mpofun |
|
531 |
530
|
a1i |
|
532 |
|
xpss |
|
533 |
472
|
inex1 |
|
534 |
533
|
mptex |
|
535 |
534
|
rgen2w |
|
536 |
449
|
dmmpoga |
|
537 |
535 536
|
mp1i |
|
538 |
532 537
|
sseqtrrid |
|
539 |
524 529 531 538
|
elovimad |
|
540 |
17
|
ad2antrr |
|
541 |
|
elrabi |
|
542 |
18
|
psrbagf |
|
543 |
541 542
|
syl |
|
544 |
543
|
ad2antll |
|
545 |
133
|
a1i |
|
546 |
494
|
adantl |
|
547 |
540 544 545 545 546
|
caofass |
|
548 |
135
|
ad2antrr |
|
549 |
80
|
adantl |
|
550 |
548 548 540 540 74 549 549
|
offval |
|
551 |
550
|
oveq2d |
|
552 |
506
|
oveq2i |
|
553 |
|
0zd |
|
554 |
|
nn0cn |
|
555 |
554
|
addridd |
|
556 |
555
|
adantl |
|
557 |
540 544 553 556
|
caofid0r |
|
558 |
552 557
|
eqtrid |
|
559 |
547 551 558
|
3eqtrrd |
|
560 |
|
oveq1 |
|
561 |
560
|
eqeq2d |
|
562 |
559 561
|
syl5ibrcom |
|
563 |
20
|
ad3antrrr |
|
564 |
18
|
psrbagaddcl |
|
565 |
458 563 564
|
syl2an2 |
|
566 |
18
|
psrbagf |
|
567 |
565 566
|
syl |
|
568 |
567
|
adantrr |
|
569 |
|
feq1 |
|
570 |
568 569
|
syl5ibrcom |
|
571 |
485 570
|
sylbid |
|
572 |
481 571
|
sylbird |
|
573 |
572
|
rexlimdvva |
|
574 |
457 573
|
mpd |
|
575 |
574
|
adantrr |
|
576 |
575
|
ffvelcdmda |
|
577 |
576
|
nn0cnd |
|
578 |
239
|
a1i |
|
579 |
577 578
|
npcand |
|
580 |
579
|
mpteq2dva |
|
581 |
575
|
ffnd |
|
582 |
581 548 540 540 74
|
offn |
|
583 |
|
eqidd |
|
584 |
581 548 540 540 74 583 549
|
ofval |
|
585 |
582 548 540 540 74 584 549
|
offval |
|
586 |
575
|
feqmptd |
|
587 |
580 585 586
|
3eqtr4rd |
|
588 |
|
oveq1 |
|
589 |
588
|
eqeq2d |
|
590 |
587 589
|
syl5ibrcom |
|
591 |
562 590
|
impbid |
|
592 |
448 523 539 591
|
f1o2d |
|
593 |
9 106 13 428 442 447 592
|
gsumf1o |
|
594 |
555
|
adantl |
|
595 |
486 488 508 594
|
caofid0r |
|
596 |
507 595
|
eqtrid |
|
597 |
496 502 596
|
3eqtrd |
|
598 |
597 514
|
eqeltrd |
|
599 |
598 517
|
syl5ibrcom |
|
600 |
599
|
adantrr |
|
601 |
485 600
|
sylbid |
|
602 |
481 601
|
sylbird |
|
603 |
602
|
rexlimdvva |
|
604 |
457 603
|
mpd |
|
605 |
|
eqidd |
|
606 |
|
eqidd |
|
607 |
|
fveq2 |
|
608 |
|
oveq2 |
|
609 |
608
|
fveq2d |
|
610 |
607 609
|
oveq12d |
|
611 |
604 605 606 610
|
fmptco |
|
612 |
6
|
ad2antrr |
|
613 |
7
|
ad2antrr |
|
614 |
|
elrabi |
|
615 |
604 614
|
syl |
|
616 |
1 2 18 612 613 615
|
psdcoef |
|
617 |
574
|
ffnd |
|
618 |
133
|
a1i |
|
619 |
618
|
ffnd |
|
620 |
17
|
ad2antrr |
|
621 |
|
eqidd |
|
622 |
|
iftrue |
|
623 |
|
1ex |
|
624 |
622 70 623
|
fvmpt |
|
625 |
624
|
adantl |
|
626 |
617 619 620 620 74 621 625
|
ofval |
|
627 |
612 626
|
mpdan |
|
628 |
627
|
oveq1d |
|
629 |
|
nn0sscn |
|
630 |
629
|
a1i |
|
631 |
574 630
|
fssd |
|
632 |
631 612
|
ffvelcdmd |
|
633 |
|
1cnd |
|
634 |
632 633
|
npcand |
|
635 |
628 634
|
eqtrd |
|
636 |
617 619 620 620 74
|
offn |
|
637 |
|
eqidd |
|
638 |
80
|
adantl |
|
639 |
617 619 620 620 74 637 638
|
ofval |
|
640 |
574
|
ffvelcdmda |
|
641 |
640
|
nn0cnd |
|
642 |
239
|
a1i |
|
643 |
641 642
|
npcand |
|
644 |
620 636 619 617 639 638 643
|
offveq |
|
645 |
644
|
fveq2d |
|
646 |
635 645
|
oveq12d |
|
647 |
616 646
|
eqtrd |
|
648 |
30
|
ad2antlr |
|
649 |
648
|
ffvelcdmda |
|
650 |
649
|
nn0cnd |
|
651 |
650 641 642
|
subsub3d |
|
652 |
651
|
mpteq2dva |
|
653 |
67
|
adantr |
|
654 |
|
eqidd |
|
655 |
653 636 620 620 74 654 639
|
offval |
|
656 |
653 619 620 620 74
|
offn |
|
657 |
653 619 620 620 74 654 638
|
ofval |
|
658 |
656 617 620 620 74 657 637
|
offval |
|
659 |
652 655 658
|
3eqtr4d |
|
660 |
659
|
fveq2d |
|
661 |
647 660
|
oveq12d |
|
662 |
11
|
ad2antrr |
|
663 |
574 612
|
ffvelcdmd |
|
664 |
663
|
nn0zd |
|
665 |
39
|
ad2antrr |
|
666 |
|
simpllr |
|
667 |
20
|
ad3antrrr |
|
668 |
|
simprl |
|
669 |
|
eqid |
|
670 |
18 245 669
|
psrbagleadd1 |
|
671 |
666 667 668 670
|
syl3anc |
|
672 |
|
eleq1 |
|
673 |
671 672
|
syl5ibrcom |
|
674 |
485 673
|
sylbid |
|
675 |
481 674
|
sylbird |
|
676 |
675
|
rexlimdvva |
|
677 |
457 676
|
mpd |
|
678 |
|
elrabi |
|
679 |
677 678
|
syl |
|
680 |
665 679
|
ffvelcdmd |
|
681 |
44
|
ad2antrr |
|
682 |
23
|
adantr |
|
683 |
18 669
|
psrbagconcl |
|
684 |
682 677 683
|
syl2anc |
|
685 |
|
elrabi |
|
686 |
684 685
|
syl |
|
687 |
681 686
|
ffvelcdmd |
|
688 |
9 26 37
|
mulgass2 |
|
689 |
662 664 680 687 688
|
syl13anc |
|
690 |
661 689
|
eqtrd |
|
691 |
690
|
mpteq2dva |
|
692 |
611 691
|
eqtrd |
|
693 |
692
|
oveq2d |
|
694 |
|
snex |
|
695 |
357 694
|
xpex |
|
696 |
695
|
funimaex |
|
697 |
530 696
|
mp1i |
|
698 |
28
|
ad2antrr |
|
699 |
9 37 662 680 687
|
ringcld |
|
700 |
9 26 698 663 699
|
mulgnn0cld |
|
701 |
|
eqid |
|
702 |
361 701
|
fnmpti |
|
703 |
702
|
a1i |
|
704 |
703 25 115
|
fndmfifsupp |
|
705 |
462
|
ad2antlr |
|
706 |
469
|
adantl |
|
707 |
472
|
a1i |
|
708 |
475
|
a1i |
|
709 |
|
eqidd |
|
710 |
|
eqidd |
|
711 |
705 706 707 708 477 709 710
|
offval |
|
712 |
711
|
eqeq2d |
|
713 |
712
|
rexbidva |
|
714 |
20
|
ad2antrr |
|
715 |
|
oveq2 |
|
716 |
715
|
eqeq2d |
|
717 |
716
|
rexsng |
|
718 |
714 717
|
syl |
|
719 |
713 718
|
bitr3d |
|
720 |
719
|
rexbidva |
|
721 |
|
breq1 |
|
722 |
|
breq1 |
|
723 |
|
fveq1 |
|
724 |
723
|
eqeq1d |
|
725 |
722 724
|
anbi12d |
|
726 |
725
|
notbid |
|
727 |
721 726
|
anbi12d |
|
728 |
458 714 564
|
syl2an2 |
|
729 |
|
simplr |
|
730 |
|
simpr |
|
731 |
18 245 46
|
psrbagleadd1 |
|
732 |
729 714 730 731
|
syl3anc |
|
733 |
721
|
elrab |
|
734 |
733
|
simprbi |
|
735 |
732 734
|
syl |
|
736 |
6
|
ad2antrr |
|
737 |
487
|
adantl |
|
738 |
737
|
ffnd |
|
739 |
135
|
ad2antrr |
|
740 |
17
|
ad2antrr |
|
741 |
|
eqidd |
|
742 |
624
|
adantl |
|
743 |
738 739 740 740 74 741 742
|
ofval |
|
744 |
736 743
|
mpdan |
|
745 |
737 736
|
ffvelcdmd |
|
746 |
|
nn0p1nn |
|
747 |
745 746
|
syl |
|
748 |
744 747
|
eqeltrd |
|
749 |
748
|
nnne0d |
|
750 |
749
|
neneqd |
|
751 |
750
|
intnand |
|
752 |
735 751
|
jca |
|
753 |
727 728 752
|
elrabd |
|
754 |
|
eleq1 |
|
755 |
753 754
|
syl5ibrcom |
|
756 |
|
breq1 |
|
757 |
|
elrabi |
|
758 |
757
|
adantl |
|
759 |
133
|
a1i |
|
760 |
757 125
|
syl |
|
761 |
760
|
adantl |
|
762 |
6
|
ad2antrr |
|
763 |
761 762
|
ffvelcdmd |
|
764 |
341
|
notbid |
|
765 |
120 764
|
anbi12d |
|
766 |
765
|
elrab |
|
767 |
766
|
simprbi |
|
768 |
767
|
simpld |
|
769 |
768
|
adantl |
|
770 |
769
|
adantr |
|
771 |
757 126
|
syl |
|
772 |
771
|
adantl |
|
773 |
772
|
adantr |
|
774 |
23
|
adantr |
|
775 |
90
|
ffnd |
|
776 |
774 775
|
syl |
|
777 |
776
|
adantr |
|
778 |
17
|
ad3antrrr |
|
779 |
|
eqidd |
|
780 |
|
eqidd |
|
781 |
773 777 778 778 74 779 780
|
ofrfval |
|
782 |
770 781
|
mpbid |
|
783 |
782
|
r19.21bi |
|
784 |
783
|
adantr |
|
785 |
67
|
ad3antrrr |
|
786 |
71
|
a1i |
|
787 |
17
|
ad4antr |
|
788 |
|
eqidd |
|
789 |
80
|
adantl |
|
790 |
785 786 787 787 74 788 789
|
ofval |
|
791 |
790
|
an32s |
|
792 |
160
|
adantl |
|
793 |
792
|
oveq2d |
|
794 |
31
|
ad2antrr |
|
795 |
794
|
ffvelcdmda |
|
796 |
795
|
adantr |
|
797 |
796
|
nn0cnd |
|
798 |
797
|
addridd |
|
799 |
791 793 798
|
3eqtrd |
|
800 |
784 799
|
breqtrd |
|
801 |
|
simpr |
|
802 |
31
|
adantr |
|
803 |
802 762
|
ffvelcdmd |
|
804 |
803
|
nn0ge0d |
|
805 |
804
|
adantr |
|
806 |
801 805
|
eqbrtrd |
|
807 |
806
|
adantr |
|
808 |
177 800 807
|
pm2.61ne |
|
809 |
808
|
ralrimiva |
|
810 |
67
|
adantr |
|
811 |
810
|
adantr |
|
812 |
|
eqidd |
|
813 |
773 811 778 778 74 779 812
|
ofrfval |
|
814 |
809 813
|
mpbird |
|
815 |
814
|
ex |
|
816 |
767
|
simprd |
|
817 |
816
|
adantl |
|
818 |
|
imnan |
|
819 |
817 818
|
sylibr |
|
820 |
819
|
con2d |
|
821 |
815 820
|
pm2.65d |
|
822 |
821
|
neqned |
|
823 |
763 822 193
|
sylanbrc |
|
824 |
823
|
nnge1d |
|
825 |
824
|
adantr |
|
826 |
175
|
breq2d |
|
827 |
825 826
|
syl5ibrcom |
|
828 |
827
|
imp |
|
829 |
761
|
ffvelcdmda |
|
830 |
829
|
nn0ge0d |
|
831 |
830
|
adantr |
|
832 |
828 831
|
ifpimpda |
|
833 |
|
brif1 |
|
834 |
832 833
|
sylibr |
|
835 |
834
|
ralrimiva |
|
836 |
71
|
a1i |
|
837 |
17
|
ad2antrr |
|
838 |
80
|
adantl |
|
839 |
|
eqidd |
|
840 |
836 772 837 837 74 838 839
|
ofrfval |
|
841 |
835 840
|
mpbird |
|
842 |
18
|
psrbagcon |
|
843 |
758 759 841 842
|
syl3anc |
|
844 |
843
|
simpld |
|
845 |
|
eqidd |
|
846 |
810 836 837 837 74 845 838
|
ofval |
|
847 |
772 776 837 837 74 839 846
|
ofrfval |
|
848 |
769 847
|
mpbid |
|
849 |
848
|
r19.21bi |
|
850 |
829
|
nn0red |
|
851 |
62
|
a1i |
|
852 |
802
|
ffvelcdmda |
|
853 |
852
|
nn0red |
|
854 |
850 851 853
|
lesubaddd |
|
855 |
849 854
|
mpbird |
|
856 |
855
|
ralrimiva |
|
857 |
772 836 837 837 74
|
offn |
|
858 |
772 836 837 837 74 839 838
|
ofval |
|
859 |
857 810 837 837 74 858 845
|
ofrfval |
|
860 |
856 859
|
mpbird |
|
861 |
756 844 860
|
elrabd |
|
862 |
829
|
nn0cnd |
|
863 |
239
|
a1i |
|
864 |
862 863
|
npcand |
|
865 |
864
|
mpteq2dva |
|
866 |
857 836 837 837 74 858 838
|
offval |
|
867 |
761
|
feqmptd |
|
868 |
865 866 867
|
3eqtr4rd |
|
869 |
|
oveq1 |
|
870 |
869
|
eqeq2d |
|
871 |
755 861 868 870
|
rspceb2dv |
|
872 |
456 720 871
|
3bitrd |
|
873 |
872
|
eqrdv |
|
874 |
|
difrab |
|
875 |
873 874
|
eqtr4di |
|
876 |
|
difssd |
|
877 |
875 876
|
eqsstrd |
|
878 |
704 877 115
|
fmptssfisupp |
|
879 |
|
difss |
|
880 |
|
disjdif |
|
881 |
|
ssdisj |
|
882 |
879 880 881
|
mp2an |
|
883 |
882
|
ineqcomi |
|
884 |
883
|
a1i |
|
885 |
281 101
|
psdmullem |
|
886 |
875 885
|
eqtr4d |
|
887 |
9 106 10 13 697 700 878 884 886
|
gsumsplit2 |
|
888 |
693 887
|
eqtrd |
|
889 |
427 593 888
|
3eqtrd |
|
890 |
417
|
adantr |
|
891 |
1 2 37 4 18 387 890 14
|
psrmulval |
|
892 |
8
|
ad2antrr |
|
893 |
1 2 18 287 892 249
|
psdcoef |
|
894 |
269
|
fveq2d |
|
895 |
894
|
oveq2d |
|
896 |
893 895
|
eqtrd |
|
897 |
896
|
oveq2d |
|
898 |
311
|
nn0zd |
|
899 |
9 26 37
|
mulgass3 |
|
900 |
226 898 230 273 899
|
syl13anc |
|
901 |
897 900
|
eqtrd |
|
902 |
901
|
mpteq2dva |
|
903 |
902
|
oveq2d |
|
904 |
9 10 13 223 323 277 284
|
gsummptfidmsplit |
|
905 |
891 903 904
|
3eqtrd |
|
906 |
421 423 424 424 425 889 905
|
offval |
|
907 |
419 906
|
eqtrd |
|
908 |
411 413 907
|
3eqtr4d |
|