Step | Hyp | Ref
| Expression |
1 | | ssid 3624 |
. 2
|
2 | | dvmptfsum.i |
. . 3
|
3 | | sseq1 3626 |
. . . . . 6
|
4 | | sumeq1 14419 |
. . . . . . . . 9
|
5 | 4 | mpteq2dv 4745 |
. . . . . . . 8
|
6 | 5 | oveq2d 6666 |
. . . . . . 7
|
7 | | sumeq1 14419 |
. . . . . . . 8
|
8 | 7 | mpteq2dv 4745 |
. . . . . . 7
|
9 | 6, 8 | eqeq12d 2637 |
. . . . . 6
|
10 | 3, 9 | imbi12d 334 |
. . . . 5
|
11 | 10 | imbi2d 330 |
. . . 4
|
12 | | sseq1 3626 |
. . . . . 6
|
13 | | sumeq1 14419 |
. . . . . . . . 9
|
14 | 13 | mpteq2dv 4745 |
. . . . . . . 8
|
15 | 14 | oveq2d 6666 |
. . . . . . 7
|
16 | | sumeq1 14419 |
. . . . . . . 8
|
17 | 16 | mpteq2dv 4745 |
. . . . . . 7
|
18 | 15, 17 | eqeq12d 2637 |
. . . . . 6
|
19 | 12, 18 | imbi12d 334 |
. . . . 5
|
20 | 19 | imbi2d 330 |
. . . 4
|
21 | | sseq1 3626 |
. . . . . 6
|
22 | | sumeq1 14419 |
. . . . . . . . 9
|
23 | 22 | mpteq2dv 4745 |
. . . . . . . 8
|
24 | 23 | oveq2d 6666 |
. . . . . . 7
|
25 | | sumeq1 14419 |
. . . . . . . 8
|
26 | 25 | mpteq2dv 4745 |
. . . . . . 7
|
27 | 24, 26 | eqeq12d 2637 |
. . . . . 6
|
28 | 21, 27 | imbi12d 334 |
. . . . 5
|
29 | 28 | imbi2d 330 |
. . . 4
|
30 | | sseq1 3626 |
. . . . . 6
|
31 | | sumeq1 14419 |
. . . . . . . . 9
|
32 | 31 | mpteq2dv 4745 |
. . . . . . . 8
|
33 | 32 | oveq2d 6666 |
. . . . . . 7
|
34 | | sumeq1 14419 |
. . . . . . . 8
|
35 | 34 | mpteq2dv 4745 |
. . . . . . 7
|
36 | 33, 35 | eqeq12d 2637 |
. . . . . 6
|
37 | 30, 36 | imbi12d 334 |
. . . . 5
|
38 | 37 | imbi2d 330 |
. . . 4
|
39 | | dvmptfsum.s |
. . . . . . 7
|
40 | | 0cnd 10033 |
. . . . . . 7
|
41 | | 0cnd 10033 |
. . . . . . . 8
|
42 | 39, 41 | dvmptc 23721 |
. . . . . . 7
|
43 | | dvmptfsum.j |
. . . . . . . . 9
↾t |
44 | | dvmptfsum.k |
. . . . . . . . . . 11
ℂfld |
45 | 44 | cnfldtopon 22586 |
. . . . . . . . . 10
TopOn |
46 | | recnprss 23668 |
. . . . . . . . . . 11
|
47 | 39, 46 | syl 17 |
. . . . . . . . . 10
|
48 | | resttopon 20965 |
. . . . . . . . . 10
TopOn
↾t TopOn |
49 | 45, 47, 48 | sylancr 695 |
. . . . . . . . 9
↾t TopOn |
50 | 43, 49 | syl5eqel 2705 |
. . . . . . . 8
TopOn |
51 | | dvmptfsum.x |
. . . . . . . 8
|
52 | | toponss 20731 |
. . . . . . . 8
TopOn |
53 | 50, 51, 52 | syl2anc 693 |
. . . . . . 7
|
54 | 39, 40, 40, 42, 53, 43, 44, 51 | dvmptres 23726 |
. . . . . 6
|
55 | | sum0 14452 |
. . . . . . . 8
|
56 | 55 | mpteq2i 4741 |
. . . . . . 7
|
57 | 56 | oveq2i 6661 |
. . . . . 6
|
58 | | sum0 14452 |
. . . . . . 7
|
59 | 58 | mpteq2i 4741 |
. . . . . 6
|
60 | 54, 57, 59 | 3eqtr4g 2681 |
. . . . 5
|
61 | 60 | a1d 25 |
. . . 4
|
62 | | ssun1 3776 |
. . . . . . . . . 10
|
63 | | sstr 3611 |
. . . . . . . . . 10
|
64 | 62, 63 | mpan 706 |
. . . . . . . . 9
|
65 | 64 | imim1i 63 |
. . . . . . . 8
|
66 | | simpll 790 |
. . . . . . . . . . . . 13
|
67 | 66, 39 | syl 17 |
. . . . . . . . . . . 12
|
68 | 2 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
69 | 64 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
70 | | ssfi 8180 |
. . . . . . . . . . . . . . 15
|
71 | 68, 69, 70 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
72 | | simp-4l 806 |
. . . . . . . . . . . . . . 15
|
73 | 69 | sselda 3603 |
. . . . . . . . . . . . . . 15
|
74 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
75 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
|
76 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . 18
|
77 | 76 | nfel1 2779 |
. . . . . . . . . . . . . . . . 17
|
78 | 75, 77 | nfim 1825 |
. . . . . . . . . . . . . . . 16
|
79 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
|
80 | 79 | 3anbi3d 1405 |
. . . . . . . . . . . . . . . . 17
|
81 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
82 | 81 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
83 | 80, 82 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
84 | | dvmptfsum.a |
. . . . . . . . . . . . . . . 16
|
85 | 78, 83, 84 | chvar 2262 |
. . . . . . . . . . . . . . 15
|
86 | 72, 73, 74, 85 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
87 | 71, 86 | fsumcl 14464 |
. . . . . . . . . . . . 13
|
88 | 87 | adantlrr 757 |
. . . . . . . . . . . 12
|
89 | | sumex 14418 |
. . . . . . . . . . . . 13
|
90 | 89 | a1i 11 |
. . . . . . . . . . . 12
|
91 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
92 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
93 | 92, 76 | nfsum 14421 |
. . . . . . . . . . . . . . . . 17
|
94 | 81 | sumeq2sdv 14435 |
. . . . . . . . . . . . . . . . 17
|
95 | 91, 93, 94 | cbvmpt 4749 |
. . . . . . . . . . . . . . . 16
|
96 | 95 | oveq2i 6661 |
. . . . . . . . . . . . . . 15
|
97 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
98 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . 17
|
99 | 92, 98 | nfsum 14421 |
. . . . . . . . . . . . . . . 16
|
100 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . 17
|
101 | 100 | sumeq2sdv 14435 |
. . . . . . . . . . . . . . . 16
|
102 | 97, 99, 101 | cbvmpt 4749 |
. . . . . . . . . . . . . . 15
|
103 | 96, 102 | eqeq12i 2636 |
. . . . . . . . . . . . . 14
|
104 | 103 | biimpi 206 |
. . . . . . . . . . . . 13
|
105 | 104 | ad2antll 765 |
. . . . . . . . . . . 12
|
106 | | simplll 798 |
. . . . . . . . . . . . . 14
|
107 | | ssun2 3777 |
. . . . . . . . . . . . . . . . 17
|
108 | | sstr 3611 |
. . . . . . . . . . . . . . . . 17
|
109 | 107, 108 | mpan 706 |
. . . . . . . . . . . . . . . 16
|
110 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
111 | 110 | snss 4316 |
. . . . . . . . . . . . . . . 16
|
112 | 109, 111 | sylibr 224 |
. . . . . . . . . . . . . . 15
|
113 | 112 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
114 | | simpr 477 |
. . . . . . . . . . . . . 14
|
115 | 84 | 3expb 1266 |
. . . . . . . . . . . . . . . . 17
|
116 | 115 | ancom2s 844 |
. . . . . . . . . . . . . . . 16
|
117 | 116 | ralrimivva 2971 |
. . . . . . . . . . . . . . 15
|
118 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . 18
|
119 | 118 | nfel1 2779 |
. . . . . . . . . . . . . . . . 17
|
120 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
121 | 120 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
122 | 77, 119, 82, 121 | rspc2 3320 |
. . . . . . . . . . . . . . . 16
|
123 | 122 | ancoms 469 |
. . . . . . . . . . . . . . 15
|
124 | 117, 123 | mpan9 486 |
. . . . . . . . . . . . . 14
|
125 | 106, 113,
114, 124 | syl12anc 1324 |
. . . . . . . . . . . . 13
|
126 | 125 | adantlrr 757 |
. . . . . . . . . . . 12
|
127 | | dvmptfsum.b |
. . . . . . . . . . . . . . . . . 18
|
128 | 127 | 3expb 1266 |
. . . . . . . . . . . . . . . . 17
|
129 | 128 | ancom2s 844 |
. . . . . . . . . . . . . . . 16
|
130 | 129 | ralrimivva 2971 |
. . . . . . . . . . . . . . 15
|
131 | 98 | nfel1 2779 |
. . . . . . . . . . . . . . . . 17
|
132 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . 18
|
133 | 132 | nfel1 2779 |
. . . . . . . . . . . . . . . . 17
|
134 | 100 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
135 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
136 | 135 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
137 | 131, 133,
134, 136 | rspc2 3320 |
. . . . . . . . . . . . . . . 16
|
138 | 137 | ancoms 469 |
. . . . . . . . . . . . . . 15
|
139 | 130, 138 | mpan9 486 |
. . . . . . . . . . . . . 14
|
140 | 106, 113,
114, 139 | syl12anc 1324 |
. . . . . . . . . . . . 13
|
141 | 140 | adantlrr 757 |
. . . . . . . . . . . 12
|
142 | 112 | ad2antrl 764 |
. . . . . . . . . . . . 13
|
143 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
|
144 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
145 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
146 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
147 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . . 19
|
148 | 146, 147 | nfmpt 4746 |
. . . . . . . . . . . . . . . . . 18
|
149 | 144, 145,
148 | nfov 6676 |
. . . . . . . . . . . . . . . . 17
|
150 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . 18
|
151 | 146, 150 | nfmpt 4746 |
. . . . . . . . . . . . . . . . 17
|
152 | 149, 151 | nfeq 2776 |
. . . . . . . . . . . . . . . 16
|
153 | 143, 152 | nfim 1825 |
. . . . . . . . . . . . . . 15
|
154 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
|
155 | 154 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
|
156 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . . 19
|
157 | 156 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . 18
|
158 | 157 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
159 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
160 | 159 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . 17
|
161 | 158, 160 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
162 | 155, 161 | imbi12d 334 |
. . . . . . . . . . . . . . 15
|
163 | | dvmptfsum.d |
. . . . . . . . . . . . . . 15
|
164 | 153, 162,
163 | chvar 2262 |
. . . . . . . . . . . . . 14
|
165 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
166 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
167 | 166, 76 | nfcsb 3551 |
. . . . . . . . . . . . . . . 16
|
168 | 81 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . 16
|
169 | 165, 167,
168 | cbvmpt 4749 |
. . . . . . . . . . . . . . 15
|
170 | 169 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
171 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
172 | 166, 98 | nfcsb 3551 |
. . . . . . . . . . . . . . 15
|
173 | 100 | csbeq2dv 3992 |
. . . . . . . . . . . . . . 15
|
174 | 171, 172,
173 | cbvmpt 4749 |
. . . . . . . . . . . . . 14
|
175 | 164, 170,
174 | 3eqtr3g 2679 |
. . . . . . . . . . . . 13
|
176 | 66, 142, 175 | syl2anc 693 |
. . . . . . . . . . . 12
|
177 | 67, 88, 90, 105, 126, 141, 176 | dvmptadd 23723 |
. . . . . . . . . . 11
|
178 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
179 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
180 | 179, 76 | nfsum 14421 |
. . . . . . . . . . . . . . 15
|
181 | 81 | sumeq2sdv 14435 |
. . . . . . . . . . . . . . 15
|
182 | 178, 180,
181 | cbvmpt 4749 |
. . . . . . . . . . . . . 14
|
183 | | simpllr 799 |
. . . . . . . . . . . . . . . . . 18
|
184 | | disjsn 4246 |
. . . . . . . . . . . . . . . . . 18
|
185 | 183, 184 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
186 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
|
187 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
|
188 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . 18
|
189 | 68, 187, 188 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
190 | | simp-4l 806 |
. . . . . . . . . . . . . . . . . 18
|
191 | 187 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
|
192 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
|
193 | 190, 191,
192, 85 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
194 | 185, 186,
189, 193 | fsumsplit 14471 |
. . . . . . . . . . . . . . . 16
|
195 | | sumsns 14479 |
. . . . . . . . . . . . . . . . . 18
|
196 | 110, 125,
195 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
197 | 196 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
198 | 194, 197 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
199 | 198 | mpteq2dva 4744 |
. . . . . . . . . . . . . 14
|
200 | 182, 199 | syl5eq 2668 |
. . . . . . . . . . . . 13
|
201 | 200 | adantrr 753 |
. . . . . . . . . . . 12
|
202 | 201 | oveq2d 6666 |
. . . . . . . . . . 11
|
203 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
204 | 179, 98 | nfsum 14421 |
. . . . . . . . . . . . . 14
|
205 | 100 | sumeq2sdv 14435 |
. . . . . . . . . . . . . 14
|
206 | 203, 204,
205 | cbvmpt 4749 |
. . . . . . . . . . . . 13
|
207 | 75, 131 | nfim 1825 |
. . . . . . . . . . . . . . . . . 18
|
208 | 80, 134 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
|
209 | 207, 208,
127 | chvar 2262 |
. . . . . . . . . . . . . . . . 17
|
210 | 190, 191,
192, 209 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
211 | 185, 186,
189, 210 | fsumsplit 14471 |
. . . . . . . . . . . . . . 15
|
212 | | sumsns 14479 |
. . . . . . . . . . . . . . . . 17
|
213 | 110, 140,
212 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
214 | 213 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
215 | 211, 214 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
216 | 215 | mpteq2dva 4744 |
. . . . . . . . . . . . 13
|
217 | 206, 216 | syl5eq 2668 |
. . . . . . . . . . . 12
|
218 | 217 | adantrr 753 |
. . . . . . . . . . 11
|
219 | 177, 202,
218 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
220 | 219 | exp32 631 |
. . . . . . . . 9
|
221 | 220 | a2d 29 |
. . . . . . . 8
|
222 | 65, 221 | syl5 34 |
. . . . . . 7
|
223 | 222 | expcom 451 |
. . . . . 6
|
224 | 223 | adantl 482 |
. . . . 5
|
225 | 224 | a2d 29 |
. . . 4
|
226 | 11, 20, 29, 38, 61, 225 | findcard2s 8201 |
. . 3
|
227 | 2, 226 | mpcom 38 |
. 2
|
228 | 1, 227 | mpi 20 |
1
|