Step | Hyp | Ref
| Expression |
1 | | relxp 5227 |
. . . . . . . . 9
|
2 | 1 | rgenw 2924 |
. . . . . . . 8
|
3 | | reliun 5239 |
. . . . . . . 8
|
4 | 2, 3 | mpbir 221 |
. . . . . . 7
|
5 | | relcnv 5503 |
. . . . . . 7
|
6 | | ancom 466 |
. . . . . . . . . . . 12
|
7 | | vex 3203 |
. . . . . . . . . . . . 13
|
8 | | vex 3203 |
. . . . . . . . . . . . 13
|
9 | 7, 8 | opth 4945 |
. . . . . . . . . . . 12
|
10 | 8, 7 | opth 4945 |
. . . . . . . . . . . 12
|
11 | 6, 9, 10 | 3bitr4i 292 |
. . . . . . . . . . 11
|
12 | 11 | a1i 11 |
. . . . . . . . . 10
|
13 | | fsumcom2.4 |
. . . . . . . . . 10
|
14 | 12, 13 | anbi12d 747 |
. . . . . . . . 9
|
15 | 14 | 2exbidv 1852 |
. . . . . . . 8
|
16 | | eliunxp 5259 |
. . . . . . . 8
|
17 | 7, 8 | opelcnv 5304 |
. . . . . . . . 9
|
18 | | eliunxp 5259 |
. . . . . . . . 9
|
19 | | excom 2042 |
. . . . . . . . 9
|
20 | 17, 18, 19 | 3bitri 286 |
. . . . . . . 8
|
21 | 15, 16, 20 | 3bitr4g 303 |
. . . . . . 7
|
22 | 4, 5, 21 | eqrelrdv 5216 |
. . . . . 6
|
23 | | nfcv 2764 |
. . . . . . 7
|
24 | | nfcv 2764 |
. . . . . . . 8
|
25 | | nfcsb1v 3549 |
. . . . . . . 8
|
26 | 24, 25 | nfxp 5142 |
. . . . . . 7
|
27 | | sneq 4187 |
. . . . . . . 8
|
28 | | csbeq1a 3542 |
. . . . . . . 8
|
29 | 27, 28 | xpeq12d 5140 |
. . . . . . 7
|
30 | 23, 26, 29 | cbviun 4557 |
. . . . . 6
|
31 | | nfcv 2764 |
. . . . . . . 8
|
32 | | nfcv 2764 |
. . . . . . . . 9
|
33 | | nfcsb1v 3549 |
. . . . . . . . 9
|
34 | 32, 33 | nfxp 5142 |
. . . . . . . 8
|
35 | | sneq 4187 |
. . . . . . . . 9
|
36 | | csbeq1a 3542 |
. . . . . . . . 9
|
37 | 35, 36 | xpeq12d 5140 |
. . . . . . . 8
|
38 | 31, 34, 37 | cbviun 4557 |
. . . . . . 7
|
39 | 38 | cnveqi 5297 |
. . . . . 6
|
40 | 22, 30, 39 | 3eqtr3g 2679 |
. . . . 5
|
41 | 40 | sumeq1d 14431 |
. . . 4
|
42 | | vex 3203 |
. . . . . . . 8
|
43 | | vex 3203 |
. . . . . . . 8
|
44 | 42, 43 | op1std 7178 |
. . . . . . 7
|
45 | 44 | csbeq1d 3540 |
. . . . . 6
|
46 | 42, 43 | op2ndd 7179 |
. . . . . . . 8
|
47 | 46 | csbeq1d 3540 |
. . . . . . 7
|
48 | 47 | csbeq2dv 3992 |
. . . . . 6
|
49 | 45, 48 | eqtrd 2656 |
. . . . 5
|
50 | 43, 42 | op2ndd 7179 |
. . . . . . 7
|
51 | 50 | csbeq1d 3540 |
. . . . . 6
|
52 | 43, 42 | op1std 7178 |
. . . . . . . 8
|
53 | 52 | csbeq1d 3540 |
. . . . . . 7
|
54 | 53 | csbeq2dv 3992 |
. . . . . 6
|
55 | 51, 54 | eqtrd 2656 |
. . . . 5
|
56 | | fsumcom2.2 |
. . . . . 6
|
57 | | snfi 8038 |
. . . . . . . 8
|
58 | | fsumcom2.1 |
. . . . . . . . . 10
|
59 | 58 | adantr 481 |
. . . . . . . . 9
|
60 | 43, 42 | opelcnv 5304 |
. . . . . . . . . . . . . . . 16
|
61 | 33, 36 | opeliunxp2f 7336 |
. . . . . . . . . . . . . . . 16
|
62 | 60, 61 | sylbbr 226 |
. . . . . . . . . . . . . . 15
|
63 | 62 | adantl 482 |
. . . . . . . . . . . . . 14
|
64 | 22 | adantr 481 |
. . . . . . . . . . . . . 14
|
65 | 63, 64 | eleqtrrd 2704 |
. . . . . . . . . . . . 13
|
66 | | eliun 4524 |
. . . . . . . . . . . . 13
|
67 | 65, 66 | sylib 208 |
. . . . . . . . . . . 12
|
68 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
69 | | opelxp 5146 |
. . . . . . . . . . . . . . . . 17
|
70 | 68, 69 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
71 | 70 | simpld 475 |
. . . . . . . . . . . . . . 15
|
72 | | elsni 4194 |
. . . . . . . . . . . . . . 15
|
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . 14
|
74 | | simpl 473 |
. . . . . . . . . . . . . 14
|
75 | 73, 74 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
76 | 75 | rexlimiva 3028 |
. . . . . . . . . . . 12
|
77 | 67, 76 | syl 17 |
. . . . . . . . . . 11
|
78 | 77 | expr 643 |
. . . . . . . . . 10
|
79 | 78 | ssrdv 3609 |
. . . . . . . . 9
|
80 | 59, 79 | ssfid 8183 |
. . . . . . . 8
|
81 | | xpfi 8231 |
. . . . . . . 8
|
82 | 57, 80, 81 | sylancr 695 |
. . . . . . 7
|
83 | 82 | ralrimiva 2966 |
. . . . . 6
|
84 | | iunfi 8254 |
. . . . . 6
|
85 | 56, 83, 84 | syl2anc 693 |
. . . . 5
|
86 | | reliun 5239 |
. . . . . . 7
|
87 | | relxp 5227 |
. . . . . . . 8
|
88 | 87 | a1i 11 |
. . . . . . 7
|
89 | 86, 88 | mprgbir 2927 |
. . . . . 6
|
90 | 89 | a1i 11 |
. . . . 5
|
91 | | simpr 477 |
. . . . . . . 8
|
92 | | eliun 4524 |
. . . . . . . 8
|
93 | 91, 92 | sylib 208 |
. . . . . . 7
|
94 | | xp2nd 7199 |
. . . . . . . . . 10
|
95 | 94 | adantl 482 |
. . . . . . . . 9
|
96 | | xp1st 7198 |
. . . . . . . . . . . 12
|
97 | 96 | adantl 482 |
. . . . . . . . . . 11
|
98 | | elsni 4194 |
. . . . . . . . . . 11
|
99 | 97, 98 | syl 17 |
. . . . . . . . . 10
|
100 | 99 | csbeq1d 3540 |
. . . . . . . . 9
|
101 | 95, 100 | eleqtrrd 2704 |
. . . . . . . 8
|
102 | 101 | rexlimiva 3028 |
. . . . . . 7
|
103 | 93, 102 | syl 17 |
. . . . . 6
|
104 | | simpl 473 |
. . . . . . . . . 10
|
105 | 99, 104 | eqeltrd 2701 |
. . . . . . . . 9
|
106 | 105 | rexlimiva 3028 |
. . . . . . . 8
|
107 | 93, 106 | syl 17 |
. . . . . . 7
|
108 | | simpl 473 |
. . . . . . . . . 10
|
109 | 25 | nfcri 2758 |
. . . . . . . . . . . 12
|
110 | 72 | equcomd 1946 |
. . . . . . . . . . . . . . . . 17
|
111 | 110, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
|
112 | 111 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
|
113 | 112 | biimpa 501 |
. . . . . . . . . . . . . 14
|
114 | 69, 113 | sylbi 207 |
. . . . . . . . . . . . 13
|
115 | 114 | a1i 11 |
. . . . . . . . . . . 12
|
116 | 109, 115 | rexlimi 3024 |
. . . . . . . . . . 11
|
117 | 67, 116 | syl 17 |
. . . . . . . . . 10
|
118 | | fsumcom2.5 |
. . . . . . . . . . . . . 14
|
119 | 118 | ralrimivva 2971 |
. . . . . . . . . . . . 13
|
120 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
|
121 | 120 | nfel1 2779 |
. . . . . . . . . . . . . . 15
|
122 | 25, 121 | nfral 2945 |
. . . . . . . . . . . . . 14
|
123 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
|
124 | 123 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
|
125 | 28, 124 | raleqbidv 3152 |
. . . . . . . . . . . . . 14
|
126 | 122, 125 | rspc 3303 |
. . . . . . . . . . . . 13
|
127 | 119, 126 | mpan9 486 |
. . . . . . . . . . . 12
|
128 | | nfcsb1v 3549 |
. . . . . . . . . . . . . 14
|
129 | 128 | nfel1 2779 |
. . . . . . . . . . . . 13
|
130 | | csbeq1a 3542 |
. . . . . . . . . . . . . 14
|
131 | 130 | eleq1d 2686 |
. . . . . . . . . . . . 13
|
132 | 129, 131 | rspc 3303 |
. . . . . . . . . . . 12
|
133 | 127, 132 | syl5com 31 |
. . . . . . . . . . 11
|
134 | 133 | impr 649 |
. . . . . . . . . 10
|
135 | 108, 77, 117, 134 | syl12anc 1324 |
. . . . . . . . 9
|
136 | 135 | ralrimivva 2971 |
. . . . . . . 8
|
137 | 136 | adantr 481 |
. . . . . . 7
|
138 | | csbeq1 3536 |
. . . . . . . . 9
|
139 | | csbeq1 3536 |
. . . . . . . . . 10
|
140 | 139 | eleq1d 2686 |
. . . . . . . . 9
|
141 | 138, 140 | raleqbidv 3152 |
. . . . . . . 8
|
142 | 141 | rspcv 3305 |
. . . . . . 7
|
143 | 107, 137,
142 | sylc 65 |
. . . . . 6
|
144 | | csbeq1 3536 |
. . . . . . . . 9
|
145 | 144 | csbeq2dv 3992 |
. . . . . . . 8
|
146 | 145 | eleq1d 2686 |
. . . . . . 7
|
147 | 146 | rspcv 3305 |
. . . . . 6
|
148 | 103, 143,
147 | sylc 65 |
. . . . 5
|
149 | 49, 55, 85, 90, 148 | fsumcnv 14504 |
. . . 4
|
150 | 41, 149 | eqtr4d 2659 |
. . 3
|
151 | | fsumcom2.3 |
. . . . . 6
|
152 | 151 | ralrimiva 2966 |
. . . . 5
|
153 | 25 | nfel1 2779 |
. . . . . 6
|
154 | 28 | eleq1d 2686 |
. . . . . 6
|
155 | 153, 154 | rspc 3303 |
. . . . 5
|
156 | 152, 155 | mpan9 486 |
. . . 4
|
157 | 55, 58, 156, 134 | fsum2d 14502 |
. . 3
|
158 | 49, 56, 80, 135 | fsum2d 14502 |
. . 3
|
159 | 150, 157,
158 | 3eqtr4d 2666 |
. 2
|
160 | | nfcv 2764 |
. . 3
|
161 | | nfcv 2764 |
. . . . 5
|
162 | 161, 120 | nfcsb 3551 |
. . . 4
|
163 | 25, 162 | nfsum 14421 |
. . 3
|
164 | | nfcv 2764 |
. . . . 5
|
165 | | nfcsb1v 3549 |
. . . . 5
|
166 | | csbeq1a 3542 |
. . . . 5
|
167 | 164, 165,
166 | cbvsumi 14427 |
. . . 4
|
168 | 123 | csbeq2dv 3992 |
. . . . . 6
|
169 | 168 | adantr 481 |
. . . . 5
|
170 | 28, 169 | sumeq12dv 14437 |
. . . 4
|
171 | 167, 170 | syl5eq 2668 |
. . 3
|
172 | 160, 163,
171 | cbvsumi 14427 |
. 2
|
173 | | nfcv 2764 |
. . 3
|
174 | 33, 128 | nfsum 14421 |
. . 3
|
175 | | nfcv 2764 |
. . . . 5
|
176 | 175, 120,
123 | cbvsumi 14427 |
. . . 4
|
177 | 130 | adantr 481 |
. . . . 5
|
178 | 36, 177 | sumeq12dv 14437 |
. . . 4
|
179 | 176, 178 | syl5eq 2668 |
. . 3
|
180 | 173, 174,
179 | cbvsumi 14427 |
. 2
|
181 | 159, 172,
180 | 3eqtr4g 2681 |
1
|