MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqcoll Unicode version

Theorem seqcoll 12512
Description: The function contains a sparse set of non-zero values to be summed. The function is an order isomorphism from the set of non-zero values of to a 1-based finite sequence, and collects these non-zero values together. Under these conditions, the sum over the values in yields the same result as the sum over the original set . (Contributed by Mario Carneiro, 2-Apr-2014.)
Hypotheses
Ref Expression
seqcoll.1
seqcoll.1b
seqcoll.c
seqcoll.a
seqcoll.2
seqcoll.3
seqcoll.4
seqcoll.5
seqcoll.6
seqcoll.7
Assertion
Ref Expression
seqcoll
Distinct variable groups:   , ,   , ,   , ,   ,   ,M,   , ,   , ,   S, ,   ,

Proof of Theorem seqcoll
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seqcoll.3 . 2
2 elfznn 11743 . . . 4
31, 2syl 16 . . 3
4 eleq1 2529 . . . . . 6
5 fveq2 5871 . . . . . . . 8
65fveq2d 5875 . . . . . . 7
7 fveq2 5871 . . . . . . 7
86, 7eqeq12d 2479 . . . . . 6
94, 8imbi12d 320 . . . . 5
109imbi2d 316 . . . 4
11 eleq1 2529 . . . . . 6
12 fveq2 5871 . . . . . . . 8
1312fveq2d 5875 . . . . . . 7
14 fveq2 5871 . . . . . . 7
1513, 14eqeq12d 2479 . . . . . 6
1611, 15imbi12d 320 . . . . 5
1716imbi2d 316 . . . 4
18 eleq1 2529 . . . . . 6
19 fveq2 5871 . . . . . . . 8
2019fveq2d 5875 . . . . . . 7
21 fveq2 5871 . . . . . . 7
2220, 21eqeq12d 2479 . . . . . 6
2318, 22imbi12d 320 . . . . 5
2423imbi2d 316 . . . 4
25 eleq1 2529 . . . . . 6
26 fveq2 5871 . . . . . . . 8
2726fveq2d 5875 . . . . . . 7
28 fveq2 5871 . . . . . . 7
2927, 28eqeq12d 2479 . . . . . 6
3025, 29imbi12d 320 . . . . 5
3130imbi2d 316 . . . 4
32 seqcoll.1 . . . . . . . . 9
33 seqcoll.a . . . . . . . . 9
34 seqcoll.4 . . . . . . . . . 10
35 seqcoll.2 . . . . . . . . . . . . 13
36 isof1o 6221 . . . . . . . . . . . . 13
3735, 36syl 16 . . . . . . . . . . . 12
38 f1of 5821 . . . . . . . . . . . 12
3937, 38syl 16 . . . . . . . . . . 11
40 elfzuz2 11720 . . . . . . . . . . . . 13
411, 40syl 16 . . . . . . . . . . . 12
42 eluzfz1 11722 . . . . . . . . . . . 12
4341, 42syl 16 . . . . . . . . . . 11
4439, 43ffvelrnd 6032 . . . . . . . . . 10
4534, 44sseldd 3504 . . . . . . . . 9
46 eluzle 11122 . . . . . . . . . . . . 13
4741, 46syl 16 . . . . . . . . . . . 12
48 elfzelz 11717 . . . . . . . . . . . . . . . . 17
4948ssriv 3507 . . . . . . . . . . . . . . . 16
50 zssre 10896 . . . . . . . . . . . . . . . 16
5149, 50sstri 3512 . . . . . . . . . . . . . . 15
5251a1i 11 . . . . . . . . . . . . . 14
53 ressxr 9658 . . . . . . . . . . . . . 14
5452, 53syl6ss 3515 . . . . . . . . . . . . 13
55 eluzelre 11120 . . . . . . . . . . . . . . . 16
5655ssriv 3507 . . . . . . . . . . . . . . 15
5734, 56syl6ss 3515 . . . . . . . . . . . . . 14
5857, 53syl6ss 3515 . . . . . . . . . . . . 13
59 eluzfz2 11723 . . . . . . . . . . . . . 14
6041, 59syl 16 . . . . . . . . . . . . 13
61 leisorel 12509 . . . . . . . . . . . . 13
6235, 54, 58, 43, 60, 61syl122anc 1237 . . . . . . . . . . . 12
6347, 62mpbid 210 . . . . . . . . . . 11
6439, 60ffvelrnd 6032 . . . . . . . . . . . . . 14
6534, 64sseldd 3504 . . . . . . . . . . . . 13
66 eluzelz 11119 . . . . . . . . . . . . 13
6765, 66syl 16 . . . . . . . . . . . 12
68 elfz5 11709 . . . . . . . . . . . 12
6945, 67, 68syl2anc 661 . . . . . . . . . . 11
7063, 69mpbird 232 . . . . . . . . . 10
71 fveq2 5871 . . . . . . . . . . . . 13
7271eleq1d 2526 . . . . . . . . . . . 12
7372imbi2d 316 . . . . . . . . . . 11
74 seqcoll.5 . . . . . . . . . . . 12
7574expcom 435 . . . . . . . . . . 11
7673, 75vtoclga 3173 . . . . . . . . . 10
7770, 76mpcom 36 . . . . . . . . 9
78 eluzelz 11119 . . . . . . . . . . . . . . . . . 18
7945, 78syl 16 . . . . . . . . . . . . . . . . 17
80 peano2zm 10932 . . . . . . . . . . . . . . . . 17
8179, 80syl 16 . . . . . . . . . . . . . . . 16
8281zred 10994 . . . . . . . . . . . . . . 15
8379zred 10994 . . . . . . . . . . . . . . 15
8467zred 10994 . . . . . . . . . . . . . . 15
8583lem1d 10504 . . . . . . . . . . . . . . 15
8682, 83, 84, 85, 63letrd 9760 . . . . . . . . . . . . . 14
87 eluz 11123 . . . . . . . . . . . . . . 15
8881, 67, 87syl2anc 661 . . . . . . . . . . . . . 14
8986, 88mpbird 232 . . . . . . . . . . . . 13
90 fzss2 11752 . . . . . . . . . . . . 13
9189, 90syl 16 . . . . . . . . . . . 12
9291sselda 3503 . . . . . . . . . . 11
93 eluzel2 11115 . . . . . . . . . . . . . . 15
9445, 93syl 16 . . . . . . . . . . . . . 14
95 elfzm11 11778 . . . . . . . . . . . . . 14
9694, 79, 95syl2anc 661 . . . . . . . . . . . . 13
97 simp3 998 . . . . . . . . . . . . . 14
98 f1ocnv 5833 . . . . . . . . . . . . . . . . . . . . . . . 24
9937, 98syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
100 f1of 5821 . . . . . . . . . . . . . . . . . . . . . . 23
10199, 100syl 16 . . . . . . . . . . . . . . . . . . . . . 22
102101ffvelrnda 6031 . . . . . . . . . . . . . . . . . . . . 21
103 elfznn 11743 . . . . . . . . . . . . . . . . . . . . 21
104102, 103syl 16 . . . . . . . . . . . . . . . . . . . 20
105104nnge1d 10603 . . . . . . . . . . . . . . . . . . 19
10635adantr 465 . . . . . . . . . . . . . . . . . . . 20
10754adantr 465 . . . . . . . . . . . . . . . . . . . 20
10858adantr 465 . . . . . . . . . . . . . . . . . . . 20
10943adantr 465 . . . . . . . . . . . . . . . . . . . 20
110 leisorel 12509 . . . . . . . . . . . . . . . . . . . 20
111106, 107, 108, 109, 102, 110syl122anc 1237 . . . . . . . . . . . . . . . . . . 19
112105, 111mpbid 210 . . . . . . . . . . . . . . . . . 18
113 f1ocnvfv2 6183 . . . . . . . . . . . . . . . . . . 19
11437, 113sylan 471 . . . . . . . . . . . . . . . . . 18
115112, 114breqtrd 4476 . . . . . . . . . . . . . . . . 17
11683adantr 465 . . . . . . . . . . . . . . . . . 18
11757sselda 3503 . . . . . . . . . . . . . . . . . 18
118116, 117lenltd 9752 . . . . . . . . . . . . . . . . 17
119115, 118mpbid 210 . . . . . . . . . . . . . . . 16
120119ex 434 . . . . . . . . . . . . . . 15
121120con2d 115 . . . . . . . . . . . . . 14
12297, 121syl5 32 . . . . . . . . . . . . 13
12396, 122sylbid 215 . . . . . . . . . . . 12
124123imp 429 . . . . . . . . . . 11
12592, 124eldifd 3486 . . . . . . . . . 10
126 seqcoll.6 . . . . . . . . . 10
127125, 126syldan 470 . . . . . . . . 9
12832, 33, 45, 77, 127seqid 12152 . . . . . . . 8
129128fveq1d 5873 . . . . . . 7
130 uzid 11124 . . . . . . . . 9
13179, 130syl 16 . . . . . . . 8
132 fvres 5885 . . . . . . . 8
133131, 132syl 16 . . . . . . 7
134 seq1 12120 . . . . . . . . 9
13579, 134syl 16 . . . . . . . 8
136 fveq2 5871 . . . . . . . . . . . 12
137 fveq2 5871 . . . . . . . . . . . . 13
138137fveq2d 5875 . . . . . . . . . . . 12
139136, 138eqeq12d 2479 . . . . . . . . . . 11
140139imbi2d 316 . . . . . . . . . 10
141 seqcoll.7 . . . . . . . . . . 11
142141expcom 435 . . . . . . . . . 10
143140, 142vtoclga 3173 . . . . . . . . 9
14443, 143mpcom 36 . . . . . . . 8
145135, 144eqtr4d 2501 . . . . . . 7
146129, 133, 1453eqtr3d 2506 . . . . . 6
147 1z 10919 . . . . . . 7
148 seq1 12120 . . . . . . 7
149147, 148ax-mp 5 . . . . . 6
150146, 149syl6eqr 2516 . . . . 5
151150a1d 25 . . . 4
152 simplr 755 . . . . . . . . . . 11
153 nnuz 11145 . . . . . . . . . . 11
154152, 153syl6eleq 2555 . . . . . . . . . 10
155 nnz 10911 . . . . . . . . . . . 12
156155ad2antlr 726 . . . . . . . . . . 11
157 elfzuz3 11714 . . . . . . . . . . . 12
158157adantl 466 . . . . . . . . . . 11
159 peano2uzr 11165 . . . . . . . . . . 11
160156, 158, 159syl2anc 661 . . . . . . . . . 10
161 elfzuzb 11711 . . . . . . . . . 10
162154, 160, 161sylanbrc 664 . . . . . . . . 9
163162ex 434 . . . . . . . 8
164163imim1d 75 . . . . . . 7
165 oveq1 6303 . . . . . . . . . 10
166 simpll 753 . . . . . . . . . . . . . . 15
167 seqcoll.1b . . . . . . . . . . . . . . 15
168166, 167sylan 471 . . . . . . . . . . . . . 14
16934ad2antrr 725 . . . . . . . . . . . . . . 15
17039ad2antrr 725 . . . . . . . . . . . . . . . 16
171170, 162ffvelrnd 6032 . . . . . . . . . . . . . . 15
172169, 171sseldd 3504 . . . . . . . . . . . . . 14
173 nnre 10568 . . . . . . . . . . . . . . . . . . 19
174173ad2antlr 726 . . . . . . . . . . . . . . . . . 18
175174ltp1d 10501 . . . . . . . . . . . . . . . . 17
17635ad2antrr 725 . . . . . . . . . . . . . . . . . 18
177 simpr 461 . . . . . . . . . . . . . . . . . 18
178 isorel 6222 . . . . . . . . . . . . . . . . . 18
179176, 162, 177, 178syl12anc 1226 . . . . . . . . . . . . . . . . 17
180175, 179mpbid 210 . . . . . . . . . . . . . . . 16
181 eluzelz 11119 . . . . . . . . . . . . . . . . . 18
182172, 181syl 16 . . . . . . . . . . . . . . . . 17
183170, 177ffvelrnd 6032 . . . . . . . . . . . . . . . . . . 19
184169, 183sseldd 3504 . . . . . . . . . . . . . . . . . 18
185 eluzelz 11119 . . . . . . . . . . . . . . . . . 18
186184, 185syl 16 . . . . . . . . . . . . . . . . 17
187 zltlem1 10941 . . . . . . . . . . . . . . . . 17
188182, 186, 187syl2anc 661 . . . . . . . . . . . . . . . 16
189180, 188mpbid 210 . . . . . . . . . . . . . . 15
190 peano2zm 10932 . . . . . . . . . . . . . . . . 17
191186, 190syl 16 . . . . . . . . . . . . . . . 16
192 eluz 11123 . . . . . . . . . . . . . . . 16
193182, 191, 192syl2anc 661 . . . . . . . . . . . . . . 15
194189, 193mpbird 232 . . . . . . . . . . . . . 14
195191zred 10994 . . . . . . . . . . . . . . . . . . . . 21
196186zred 10994 . . . . . . . . . . . . . . . . . . . . 21
19784ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
198196lem1d 10504 . . . . . . . . . . . . . . . . . . . . 21
199 elfzle2 11719 . . . . . . . . . . . . . . . . . . . . . . 23
200199adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
20154ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
20258ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
20360ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
204 leisorel 12509 . . . . . . . . . . . . . . . . . . . . . . 23
205176, 201, 202, 177, 203, 204syl122anc 1237 . . . . . . . . . . . . . . . . . . . . . 22
206200, 205mpbid 210 . . . . . . . . . . . . . . . . . . . . 21
207195, 196, 197, 198, 206letrd 9760 . . . . . . . . . . . . . . . . . . . 20
20867ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
209 eluz 11123 . . . . . . . . . . . . . . . . . . . . 21
210191, 208, 209syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
211207, 210mpbird 232 . . . . . . . . . . . . . . . . . . 19
212 uztrn 11126 . . . . . . . . . . . . . . . . . . 19
213211, 194, 212syl2anc 661 . . . . . . . . . . . . . . . . . 18
214 fzss2 11752 . . . . . . . . . . . . . . . . . 18
215213, 214syl 16 . . . . . . . . . . . . . . . . 17
216215sselda 3503 . . . . . . . . . . . . . . . 16
217166, 74sylan 471 . . . . . . . . . . . . . . . 16
218216, 217syldan 470 . . . . . . . . . . . . . . 15
219 seqcoll.c . . . . . . . . . . . . . . . 16
220166, 219sylan 471 . . . . . . . . . . . . . . 15
221172, 218, 220seqcl 12127 . . . . . . . . . . . . . 14
222 simplll 759 . . . . . . . . . . . . . . 15
223 elfzuz 11713 . . . . . . . . . . . . . . . . . 18
224 peano2uz 11163 . . . . . . . . . . . . . . . . . . 19
225172, 224syl 16 . . . . . . . . . . . . . . . . . 18
226 uztrn 11126 . . . . . . . . . . . . . . . . . 18