Step Hyp Ref
Expression 1 relxp 5115 . . . . . . . . 9
2 1 rgenw 2818 . . . . . . . 8
3 reliun 5128 . . . . . . . 8
4 2 , 3 mpbir 209 . . . . . . 7
5 relcnv 5379 . . . . . . 7
6 ancom 450 . . . . . . . . . . . 12
7 vex 3112 . . . . . . . . . . . . 13
8 vex 3112 . . . . . . . . . . . . 13
9 7 , 8 opth 4726 . . . . . . . . . . . 12
10 8 , 7 opth 4726 . . . . . . . . . . . 12
11 6 , 9 , 10 3bitr4i 277 . . . . . . . . . . 11
12 11 a1i 11 . . . . . . . . . 10
13 fsumcom2.4 . . . . . . . . . 10
14 12 , 13 anbi12d 710 . . . . . . . . 9
15 14 2exbidv 1716 . . . . . . . 8
16 eliunxp 5145 . . . . . . . 8
17 7 , 8 opelcnv 5189 . . . . . . . . 9
18 eliunxp 5145 . . . . . . . . 9
19 excom 1849 . . . . . . . . 9
20 17 , 18 , 19 3bitri 271 . . . . . . . 8
21 15 , 16 , 20 3bitr4g 288 . . . . . . 7
22 4 , 5 , 21 eqrelrdv 5104 . . . . . 6
23 nfcv 2619 . . . . . . 7
24 nfcv 2619 . . . . . . . 8
25 nfcsb1v 3450 . . . . . . . 8
26 24 , 25 nfxp 5031 . . . . . . 7
27 sneq 4039 . . . . . . . 8
28 csbeq1a 3443 . . . . . . . 8
29 27 , 28 xpeq12d 5029 . . . . . . 7
30 23 , 26 , 29 cbviun 4367 . . . . . 6
31 nfcv 2619 . . . . . . . 8
32 nfcv 2619 . . . . . . . . 9
33 nfcsb1v 3450 . . . . . . . . 9
34 32 , 33 nfxp 5031 . . . . . . . 8
35 sneq 4039 . . . . . . . . 9
36 csbeq1a 3443 . . . . . . . . 9
37 35 , 36 xpeq12d 5029 . . . . . . . 8
38 31 , 34 , 37 cbviun 4367 . . . . . . 7
39 38 cnveqi 5182 . . . . . 6
40 22 , 30 , 39 3eqtr3g 2521 . . . . 5
41 40 sumeq1d 13523 . . . 4
42 vex 3112 . . . . . . . 8
43 vex 3112 . . . . . . . 8
44 42 , 43 op1std 6810 . . . . . . 7
45 44 csbeq1d 3441 . . . . . 6
46 42 , 43 op2ndd 6811 . . . . . . . 8
47 46 csbeq1d 3441 . . . . . . 7
48 47 csbeq2dv 3835 . . . . . 6
49 45 , 48 eqtrd 2498 . . . . 5
50 43 , 42 op2ndd 6811 . . . . . . 7
51 50 csbeq1d 3441 . . . . . 6
52 43 , 42 op1std 6810 . . . . . . . 8
53 52 csbeq1d 3441 . . . . . . 7
54 53 csbeq2dv 3835 . . . . . 6
55 51 , 54 eqtrd 2498 . . . . 5
56 fsumcom2.2 . . . . . 6
57 snfi 7616 . . . . . . . 8
58 fsumcom2.1 . . . . . . . . . 10
59 58 adantr 465 . . . . . . . . 9
60 33 nfcri 2612 . . . . . . . . . . . . . . . . . 18
61 id 22 . . . . . . . . . . . . . . . . . . . . . 22
62 ssnid 4058 . . . . . . . . . . . . . . . . . . . . . 22
63 61 , 62 syl6eqelr 2554 . . . . . . . . . . . . . . . . . . . . 21
64 63 biantrurd 508 . . . . . . . . . . . . . . . . . . . 20
65 opelxp 5034 . . . . . . . . . . . . . . . . . . . 20
66 64 , 65 syl6rbbr 264 . . . . . . . . . . . . . . . . . . 19
67 36 eleq2d 2527 . . . . . . . . . . . . . . . . . . 19
68 66 , 67 bitrd 253 . . . . . . . . . . . . . . . . . 18
69 60 , 68 rspce 3205 . . . . . . . . . . . . . . . . 17
70 eliun 4335 . . . . . . . . . . . . . . . . 17
71 69 , 70 sylibr 212 . . . . . . . . . . . . . . . 16
72 43 , 42 opelcnv 5189 . . . . . . . . . . . . . . . 16
73 71 , 72 sylibr 212 . . . . . . . . . . . . . . 15
74 73 adantl 466 . . . . . . . . . . . . . 14
75 22 adantr 465 . . . . . . . . . . . . . 14
76 74 , 75 eleqtrrd 2548 . . . . . . . . . . . . 13
77 eliun 4335 . . . . . . . . . . . . 13
78 76 , 77 sylib 196 . . . . . . . . . . . 12
79 simpr 461 . . . . . . . . . . . . . . . . 17
80 opelxp 5034 . . . . . . . . . . . . . . . . 17
81 79 , 80 sylib 196 . . . . . . . . . . . . . . . 16
82 81 simpld 459 . . . . . . . . . . . . . . 15
83 elsni 4054 . . . . . . . . . . . . . . 15
84 82 , 83 syl 16 . . . . . . . . . . . . . 14
85 simpl 457 . . . . . . . . . . . . . 14
86 84 , 85 eqeltrd 2545 . . . . . . . . . . . . 13
87 86 rexlimiva 2945 . . . . . . . . . . . 12
88 78 , 87 syl 16 . . . . . . . . . . 11
89 88 expr 615 . . . . . . . . . 10
90 89 ssrdv 3509 . . . . . . . . 9
91 ssfi 7760 . . . . . . . . 9
92 59 , 90 , 91 syl2anc 661 . . . . . . . 8
93 xpfi 7811 . . . . . . . 8
94 57 , 92 , 93 sylancr 663 . . . . . . 7
95 94 ralrimiva 2871 . . . . . 6
96 iunfi 7828 . . . . . 6
97 56 , 95 , 96 syl2anc 661 . . . . 5
98 reliun 5128 . . . . . . 7
99 relxp 5115 . . . . . . . 8
100 99 a1i 11 . . . . . . 7
101 98 , 100 mprgbir 2821 . . . . . 6
102 101 a1i 11 . . . . 5
103 simpr 461 . . . . . . . 8
104 eliun 4335 . . . . . . . 8
105 103 , 104 sylib 196 . . . . . . 7
106 xp2nd 6831 . . . . . . . . . 10
107 106 adantl 466 . . . . . . . . 9
108 xp1st 6830 . . . . . . . . . . . 12
109 108 adantl 466 . . . . . . . . . . 11
110 elsni 4054 . . . . . . . . . . 11
111 109 , 110 syl 16 . . . . . . . . . 10
112 111 csbeq1d 3441 . . . . . . . . 9
113 107 , 112 eleqtrrd 2548 . . . . . . . 8
114 113 rexlimiva 2945 . . . . . . 7
115 105 , 114 syl 16 . . . . . 6
116 simpl 457 . . . . . . . . . 10
117 111 , 116 eqeltrd 2545 . . . . . . . . 9
118 117 rexlimiva 2945 . . . . . . . 8
119 105 , 118 syl 16 . . . . . . 7
120 simpl 457 . . . . . . . . . 10
121 25 nfcri 2612 . . . . . . . . . . . 12
122 83 eqcomd 2465 . . . . . . . . . . . . . . . . 17
123 122 , 28 syl 16 . . . . . . . . . . . . . . . 16
124 123 eleq2d 2527 . . . . . . . . . . . . . . 15
125 124 biimpa 484 . . . . . . . . . . . . . 14
126 80 , 125 sylbi 195 . . . . . . . . . . . . 13
127 126 a1i 11 . . . . . . . . . . . 12
128 121 , 127 rexlimi 2939 . . . . . . . . . . 11
129 78 , 128 syl 16 . . . . . . . . . 10
130 fsumcom2.5 . . . . . . . . . . . . . 14
131 130 ralrimivva 2878 . . . . . . . . . . . . 13
132 nfcsb1v 3450 . . . . . . . . . . . . . . . 16
133 132 nfel1 2635 . . . . . . . . . . . . . . 15
134 25 , 133 nfral 2843 . . . . . . . . . . . . . 14
135 csbeq1a 3443 . . . . . . . . . . . . . . . 16
136 135 eleq1d 2526 . . . . . . . . . . . . . . 15
137 28 , 136 raleqbidv 3068 . . . . . . . . . . . . . 14
138 134 , 137 rspc 3204 . . . . . . . . . . . . 13
139 131 , 138 mpan9 469 . . . . . . . . . . . 12
140 nfcsb1v 3450 . . . . . . . . . . . . . 14
141 140 nfel1 2635 . . . . . . . . . . . . 13
142 csbeq1a 3443 . . . . . . . . . . . . . 14
143 142 eleq1d 2526 . . . . . . . . . . . . 13
144 141 , 143 rspc 3204 . . . . . . . . . . . 12
145 139 , 144 syl5com 30 . . . . . . . . . . 11
146 145 impr 619 . . . . . . . . . 10
147 120 , 88 , 129 , 146 syl12anc 1226 . . . . . . . . 9
148 147 ralrimivva 2878 . . . . . . . 8
149 148 adantr 465 . . . . . . 7
150 csbeq1 3437 . . . . . . . . 9
151 csbeq1 3437 . . . . . . . . . 10
152 151 eleq1d 2526 . . . . . . . . 9
153 150 , 152 raleqbidv 3068 . . . . . . . 8
154 153 rspcv 3206 . . . . . . 7
155 119 , 149 ,
154 sylc 60 . . . . . 6
156 csbeq1 3437 . . . . . . . . 9
157 156 csbeq2dv 3835 . . . . . . . 8
158 157 eleq1d 2526 . . . . . . 7
159 158 rspcv 3206 . . . . . 6
160 115 , 155 ,
159 sylc 60 . . . . 5
161 49 , 55 , 97 , 102 , 160 fsumcnv 13588 . . . 4
162 41 , 161 eqtr4d 2501 . . 3
163 fsumcom2.3 . . . . . 6
164 163 ralrimiva 2871 . . . . 5
165 25 nfel1 2635 . . . . . 6
166 28 eleq1d 2526 . . . . . 6
167 165 , 166 rspc 3204 . . . . 5
168 164 , 167 mpan9 469 . . . 4
169 55 , 58 , 168 , 146 fsum2d 13586 . . 3
170 49 , 56 , 92 , 147 fsum2d 13586 . . 3
171 162 , 169 ,
170 3eqtr4d 2508 . 2
172 nfcv 2619 . . 3
173 nfcv 2619 . . . . 5
174 173 , 132 nfcsb 3452 . . . 4
175 25 , 174 nfsum 13513 . . 3
176 nfcv 2619 . . . . 5
177 nfcsb1v 3450 . . . . 5
178 csbeq1a 3443 . . . . 5
179 176 , 177 ,
178 cbvsumi 13519 . . . 4
180 135 csbeq2dv 3835 . . . . . 6
181 180 adantr 465 . . . . 5
182 28 , 181 sumeq12dv 13528 . . . 4
183 179 , 182 syl5eq 2510 . . 3
184 172 , 175 ,
183 cbvsumi 13519 . 2
185 nfcv 2619 . . 3
186 33 , 140 nfsum 13513 . . 3
187 nfcv 2619 . . . . 5
188 187 , 132 ,
135 cbvsumi 13519 . . . 4
189 142 adantr 465 . . . . 5
190 36 , 189 sumeq12dv 13528 . . . 4
191 188 , 190 syl5eq 2510 . . 3
192 185 , 186 ,
191 cbvsumi 13519 . 2
193 171 , 184 ,
192 3eqtr4g 2523 1
