Step | Hyp | Ref
| Expression |
1 | | eluzelz 11697 |
. . . . . . . . . . . . 13
|
2 | 1 | adantl 482 |
. . . . . . . . . . . 12
|
3 | | nfra1 2941 |
. . . . . . . . . . . . . . . . 17
|
4 | | rsp 2929 |
. . . . . . . . . . . . . . . . . . . . 21
|
5 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
6 | | ifeq1 4090 |
. . . . . . . . . . . . . . . . . . . 20
|
7 | 5, 6 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
|
8 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . 20
|
9 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . 20
|
10 | 8, 9 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . 19
|
11 | 7, 10 | pm2.61d1 171 |
. . . . . . . . . . . . . . . . . 18
|
12 | | fvif 6204 |
. . . . . . . . . . . . . . . . . 18
|
13 | | fvif 6204 |
. . . . . . . . . . . . . . . . . 18
|
14 | 11, 12, 13 | 3eqtr4g 2681 |
. . . . . . . . . . . . . . . . 17
|
15 | 3, 14 | mpteq2da 4743 |
. . . . . . . . . . . . . . . 16
|
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . 15
|
17 | 16 | fveq1d 6193 |
. . . . . . . . . . . . . 14
|
18 | 17 | adantlr 751 |
. . . . . . . . . . . . 13
|
19 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
20 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
21 | 19, 20 | fvmptex 6294 |
. . . . . . . . . . . . 13
|
22 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
23 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
24 | 22, 23 | fvmptex 6294 |
. . . . . . . . . . . . 13
|
25 | 18, 21, 24 | 3eqtr4g 2681 |
. . . . . . . . . . . 12
|
26 | 2, 25 | seqfeq 12826 |
. . . . . . . . . . 11
|
27 | 26 | breq1d 4663 |
. . . . . . . . . 10
|
28 | 27 | anbi2d 740 |
. . . . . . . . 9
|
29 | 28 | exbidv 1850 |
. . . . . . . 8
|
30 | 29 | rexbidva 3049 |
. . . . . . 7
|
31 | 30 | adantr 481 |
. . . . . 6
|
32 | | simpr 477 |
. . . . . . . 8
|
33 | 15 | adantr 481 |
. . . . . . . . . . 11
|
34 | 33 | fveq1d 6193 |
. . . . . . . . . 10
|
35 | 34, 21, 24 | 3eqtr4g 2681 |
. . . . . . . . 9
|
36 | 35 | adantlr 751 |
. . . . . . . 8
|
37 | 32, 36 | seqfeq 12826 |
. . . . . . 7
|
38 | 37 | breq1d 4663 |
. . . . . 6
|
39 | 31, 38 | 3anbi23d 1402 |
. . . . 5
|
40 | 39 | rexbidva 3049 |
. . . 4
|
41 | | simplr 792 |
. . . . . . . . . 10
|
42 | | nnuz 11723 |
. . . . . . . . . 10
|
43 | 41, 42 | syl6eleq 2711 |
. . . . . . . . 9
|
44 | | f1of 6137 |
. . . . . . . . . . . . . 14
|
45 | 44 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
46 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
|
47 | 45, 46 | sylancom 701 |
. . . . . . . . . . . 12
|
48 | | simplll 798 |
. . . . . . . . . . . 12
|
49 | | nfcsb1v 3549 |
. . . . . . . . . . . . . 14
|
50 | | nfcsb1v 3549 |
. . . . . . . . . . . . . 14
|
51 | 49, 50 | nfeq 2776 |
. . . . . . . . . . . . 13
|
52 | | csbeq1a 3542 |
. . . . . . . . . . . . . 14
|
53 | | csbeq1a 3542 |
. . . . . . . . . . . . . 14
|
54 | 52, 53 | eqeq12d 2637 |
. . . . . . . . . . . . 13
|
55 | 51, 54 | rspc 3303 |
. . . . . . . . . . . 12
|
56 | 47, 48, 55 | sylc 65 |
. . . . . . . . . . 11
|
57 | | fvex 6201 |
. . . . . . . . . . . 12
|
58 | | csbfv2g 6232 |
. . . . . . . . . . . 12
|
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . 11
|
60 | | csbfv2g 6232 |
. . . . . . . . . . . 12
|
61 | 57, 60 | ax-mp 5 |
. . . . . . . . . . 11
|
62 | 56, 59, 61 | 3eqtr3g 2679 |
. . . . . . . . . 10
|
63 | | elfznn 12370 |
. . . . . . . . . . . 12
|
64 | 63 | adantl 482 |
. . . . . . . . . . 11
|
65 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
66 | 65 | csbeq1d 3540 |
. . . . . . . . . . . 12
|
67 | | eqid 2622 |
. . . . . . . . . . . 12
|
68 | 66, 67 | fvmpti 6281 |
. . . . . . . . . . 11
|
69 | 64, 68 | syl 17 |
. . . . . . . . . 10
|
70 | 65 | csbeq1d 3540 |
. . . . . . . . . . . 12
|
71 | | eqid 2622 |
. . . . . . . . . . . 12
|
72 | 70, 71 | fvmpti 6281 |
. . . . . . . . . . 11
|
73 | 64, 72 | syl 17 |
. . . . . . . . . 10
|
74 | 62, 69, 73 | 3eqtr4d 2666 |
. . . . . . . . 9
|
75 | 43, 74 | seqfveq 12825 |
. . . . . . . 8
|
76 | 75 | eqeq2d 2632 |
. . . . . . 7
|
77 | 76 | pm5.32da 673 |
. . . . . 6
|
78 | 77 | exbidv 1850 |
. . . . 5
|
79 | 78 | rexbidva 3049 |
. . . 4
|
80 | 40, 79 | orbi12d 746 |
. . 3
|
81 | 80 | iotabidv 5872 |
. 2
|
82 | | df-prod 14636 |
. 2
|
83 | | df-prod 14636 |
. 2
|
84 | 81, 82, 83 | 3eqtr4g 2681 |
1
|