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

Theorem seqcoll 12610
 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:   ,,   ,,   ,,   ,   ,,   ,,   ,,   ,,   ,
Allowed substitution hints:   ()   (,)   ()

Proof of Theorem seqcoll
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seqcoll.3 . 2
2 elfznn 11815 . . . 4
31, 2syl 17 . . 3
4 eleq1 2492 . . . . . 6
5 fveq2 5872 . . . . . . . 8
65fveq2d 5876 . . . . . . 7
7 fveq2 5872 . . . . . . 7
86, 7eqeq12d 2442 . . . . . 6
94, 8imbi12d 321 . . . . 5
109imbi2d 317 . . . 4
11 eleq1 2492 . . . . . 6
12 fveq2 5872 . . . . . . . 8
1312fveq2d 5876 . . . . . . 7
14 fveq2 5872 . . . . . . 7
1513, 14eqeq12d 2442 . . . . . 6
1611, 15imbi12d 321 . . . . 5
1716imbi2d 317 . . . 4
18 eleq1 2492 . . . . . 6
19 fveq2 5872 . . . . . . . 8
2019fveq2d 5876 . . . . . . 7
21 fveq2 5872 . . . . . . 7
2220, 21eqeq12d 2442 . . . . . 6
2318, 22imbi12d 321 . . . . 5
2423imbi2d 317 . . . 4
25 eleq1 2492 . . . . . 6
26 fveq2 5872 . . . . . . . 8
2726fveq2d 5876 . . . . . . 7
28 fveq2 5872 . . . . . . 7
2927, 28eqeq12d 2442 . . . . . 6
3025, 29imbi12d 321 . . . . 5
3130imbi2d 317 . . . 4
32 seqcoll.1 . . . . . . . . 9
33 seqcoll.a . . . . . . . . 9
34 seqcoll.4 . . . . . . . . . 10
35 seqcoll.2 . . . . . . . . . . . . 13
36 isof1o 6222 . . . . . . . . . . . . 13
3735, 36syl 17 . . . . . . . . . . . 12
38 f1of 5822 . . . . . . . . . . . 12
3937, 38syl 17 . . . . . . . . . . 11
40 elfzuz2 11791 . . . . . . . . . . . . 13
411, 40syl 17 . . . . . . . . . . . 12
42 eluzfz1 11793 . . . . . . . . . . . 12
4341, 42syl 17 . . . . . . . . . . 11
4439, 43ffvelrnd 6029 . . . . . . . . . 10
4534, 44sseldd 3462 . . . . . . . . 9
46 eluzle 11160 . . . . . . . . . . . . 13
4741, 46syl 17 . . . . . . . . . . . 12
48 elfzelz 11787 . . . . . . . . . . . . . . . . 17
4948ssriv 3465 . . . . . . . . . . . . . . . 16
50 zssre 10933 . . . . . . . . . . . . . . . 16
5149, 50sstri 3470 . . . . . . . . . . . . . . 15
5251a1i 11 . . . . . . . . . . . . . 14
53 ressxr 9673 . . . . . . . . . . . . . 14
5452, 53syl6ss 3473 . . . . . . . . . . . . 13
55 eluzelre 11158 . . . . . . . . . . . . . . . 16
5655ssriv 3465 . . . . . . . . . . . . . . 15
5734, 56syl6ss 3473 . . . . . . . . . . . . . 14
5857, 53syl6ss 3473 . . . . . . . . . . . . 13
59 eluzfz2 11794 . . . . . . . . . . . . . 14
6041, 59syl 17 . . . . . . . . . . . . 13
61 leisorel 12607 . . . . . . . . . . . . 13
6235, 54, 58, 43, 60, 61syl122anc 1273 . . . . . . . . . . . 12
6347, 62mpbid 213 . . . . . . . . . . 11
6439, 60ffvelrnd 6029 . . . . . . . . . . . . . 14
6534, 64sseldd 3462 . . . . . . . . . . . . 13
66 eluzelz 11157 . . . . . . . . . . . . 13
6765, 66syl 17 . . . . . . . . . . . 12
68 elfz5 11779 . . . . . . . . . . . 12
6945, 67, 68syl2anc 665 . . . . . . . . . . 11
7063, 69mpbird 235 . . . . . . . . . 10
71 fveq2 5872 . . . . . . . . . . . . 13
7271eleq1d 2489 . . . . . . . . . . . 12
7372imbi2d 317 . . . . . . . . . . 11
74 seqcoll.5 . . . . . . . . . . . 12
7574expcom 436 . . . . . . . . . . 11
7673, 75vtoclga 3142 . . . . . . . . . 10
7770, 76mpcom 37 . . . . . . . . 9
78 eluzelz 11157 . . . . . . . . . . . . . . . . . 18
7945, 78syl 17 . . . . . . . . . . . . . . . . 17
80 peano2zm 10969 . . . . . . . . . . . . . . . . 17
8179, 80syl 17 . . . . . . . . . . . . . . . 16
8281zred 11029 . . . . . . . . . . . . . . 15
8379zred 11029 . . . . . . . . . . . . . . 15
8467zred 11029 . . . . . . . . . . . . . . 15
8583lem1d 10529 . . . . . . . . . . . . . . 15
8682, 83, 84, 85, 63letrd 9781 . . . . . . . . . . . . . 14
87 eluz 11161 . . . . . . . . . . . . . . 15
8881, 67, 87syl2anc 665 . . . . . . . . . . . . . 14
8986, 88mpbird 235 . . . . . . . . . . . . 13
90 fzss2 11825 . . . . . . . . . . . . 13
9189, 90syl 17 . . . . . . . . . . . 12
9291sselda 3461 . . . . . . . . . . 11
93 eluzel2 11153 . . . . . . . . . . . . . . 15
9445, 93syl 17 . . . . . . . . . . . . . 14
95 elfzm11 11852 . . . . . . . . . . . . . 14
9694, 79, 95syl2anc 665 . . . . . . . . . . . . 13
97 simp3 1007 . . . . . . . . . . . . . 14
98 f1ocnv 5834 . . . . . . . . . . . . . . . . . . . . . . . 24
9937, 98syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
100 f1of 5822 . . . . . . . . . . . . . . . . . . . . . . 23
10199, 100syl 17 . . . . . . . . . . . . . . . . . . . . . 22
102101ffvelrnda 6028 . . . . . . . . . . . . . . . . . . . . 21
103 elfznn 11815 . . . . . . . . . . . . . . . . . . . . 21
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . 20
105104nnge1d 10641 . . . . . . . . . . . . . . . . . . 19
10635adantr 466 . . . . . . . . . . . . . . . . . . . 20
10754adantr 466 . . . . . . . . . . . . . . . . . . . 20
10858adantr 466 . . . . . . . . . . . . . . . . . . . 20
10943adantr 466 . . . . . . . . . . . . . . . . . . . 20
110 leisorel 12607 . . . . . . . . . . . . . . . . . . . 20
111106, 107, 108, 109, 102, 110syl122anc 1273 . . . . . . . . . . . . . . . . . . 19
112105, 111mpbid 213 . . . . . . . . . . . . . . . . . 18
113 f1ocnvfv2 6182 . . . . . . . . . . . . . . . . . . 19
11437, 113sylan 473 . . . . . . . . . . . . . . . . . 18
115112, 114breqtrd 4441 . . . . . . . . . . . . . . . . 17
11683adantr 466 . . . . . . . . . . . . . . . . . 18
11757sselda 3461 . . . . . . . . . . . . . . . . . 18
118116, 117lenltd 9770 . . . . . . . . . . . . . . . . 17
119115, 118mpbid 213 . . . . . . . . . . . . . . . 16
120119ex 435 . . . . . . . . . . . . . . 15
121120con2d 118 . . . . . . . . . . . . . 14
12297, 121syl5 33 . . . . . . . . . . . . 13
12396, 122sylbid 218 . . . . . . . . . . . 12
124123imp 430 . . . . . . . . . . 11
12592, 124eldifd 3444 . . . . . . . . . 10
126 seqcoll.6 . . . . . . . . . 10
127125, 126syldan 472 . . . . . . . . 9
12832, 33, 45, 77, 127seqid 12244 . . . . . . . 8
129128fveq1d 5874 . . . . . . 7
130 uzid 11162 . . . . . . . . 9
13179, 130syl 17 . . . . . . . 8
132 fvres 5886 . . . . . . . 8
133131, 132syl 17 . . . . . . 7
134 seq1 12212 . . . . . . . . 9
13579, 134syl 17 . . . . . . . 8
136 fveq2 5872 . . . . . . . . . . . 12
137 fveq2 5872 . . . . . . . . . . . . 13
138137fveq2d 5876 . . . . . . . . . . . 12
139136, 138eqeq12d 2442 . . . . . . . . . . 11
140139imbi2d 317 . . . . . . . . . 10
141 seqcoll.7 . . . . . . . . . . 11
142141expcom 436 . . . . . . . . . 10
143140, 142vtoclga 3142 . . . . . . . . 9
14443, 143mpcom 37 . . . . . . . 8
145135, 144eqtr4d 2464 . . . . . . 7
146129, 133, 1453eqtr3d 2469 . . . . . 6
147 1z 10956 . . . . . . 7
148 seq1 12212 . . . . . . 7
149147, 148ax-mp 5 . . . . . 6
150146, 149syl6eqr 2479 . . . . 5
151150a1d 26 . . . 4
152 simplr 760 . . . . . . . . . . 11
153 nnuz 11183 . . . . . . . . . . 11
154152, 153syl6eleq 2518 . . . . . . . . . 10
155 nnz 10948 . . . . . . . . . . . 12
156155ad2antlr 731 . . . . . . . . . . 11
157 elfzuz3 11784 . . . . . . . . . . . 12
158157adantl 467 . . . . . . . . . . 11
159 peano2uzr 11203 . . . . . . . . . . 11
160156, 158, 159syl2anc 665 . . . . . . . . . 10
161 elfzuzb 11781 . . . . . . . . . 10
162154, 160, 161sylanbrc 668 . . . . . . . . 9
163162ex 435 . . . . . . . 8
164163imim1d 78 . . . . . . 7
165 oveq1 6303 . . . . . . . . . 10
166 simpll 758 . . . . . . . . . . . . . . 15
167 seqcoll.1b . . . . . . . . . . . . . . 15
168166, 167sylan 473 . . . . . . . . . . . . . 14
16934ad2antrr 730 . . . . . . . . . . . . . . 15
17039ad2antrr 730 . . . . . . . . . . . . . . . 16
171170, 162ffvelrnd 6029 . . . . . . . . . . . . . . 15
172169, 171sseldd 3462 . . . . . . . . . . . . . 14
173 nnre 10605 . . . . . . . . . . . . . . . . . . 19
174173ad2antlr 731 . . . . . . . . . . . . . . . . . 18
175174ltp1d 10526 . . . . . . . . . . . . . . . . 17
17635ad2antrr 730 . . . . . . . . . . . . . . . . . 18
177 simpr 462 . . . . . . . . . . . . . . . . . 18
178 isorel 6223 . . . . . . . . . . . . . . . . . 18
179176, 162, 177, 178syl12anc 1262 . . . . . . . . . . . . . . . . 17
180175, 179mpbid 213 . . . . . . . . . . . . . . . 16
181 eluzelz 11157 . . . . . . . . . . . . . . . . . 18
182172, 181syl 17 . . . . . . . . . . . . . . . . 17
183170, 177ffvelrnd 6029 . . . . . . . . . . . . . . . . . . 19
184169, 183sseldd 3462 . . . . . . . . . . . . . . . . . 18
185 eluzelz 11157 . . . . . . . . . . . . . . . . . 18
186184, 185syl 17 . . . . . . . . . . . . . . . . 17
187 zltlem1 10978 . . . . . . . . . . . . . . . . 17
188182, 186, 187syl2anc 665 . . . . . . . . . . . . . . . 16
189180, 188mpbid 213 . . . . . . . . . . . . . . 15
190 peano2zm 10969 . . . . . . . . . . . . . . . . 17
191186, 190syl 17 . . . . . . . . . . . . . . . 16
192 eluz 11161 . . . . . . . . . . . . . . . 16
193182, 191, 192syl2anc 665 . . . . . . . . . . . . . . 15
194189, 193mpbird 235 . . . . . . . . . . . . . 14
195191zred 11029 . . . . . . . . . . . . . . . . . . . . 21
196186zred 11029 . . . . . . . . . . . . . . . . . . . . 21
19784ad2antrr 730 . . . . . . . . . . . . . . . . . . . . 21
198196lem1d 10529 . . . . . . . . . . . . . . . . . . . . 21
199 elfzle2 11790 . . . . . . . . . . . . . . . . . . . . . . 23
200199adantl 467 . . . . . . . . . . . . . . . . . . . . . 22
20154ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . 23
20258ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . 23
20360ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . 23
204 leisorel 12607 . . . . . . . . . . . . . . . . . . . . . . 23
205176, 201, 202, 177, 203, 204syl122anc 1273 . . . . . . . . . . . . . . . . . . . . . 22
206200, 205mpbid 213 . . . . . . . . . . . . . . . . . . . . 21
207195, 196, 197, 198, 206letrd 9781 . . . . . . . . . . . . . . . . . . . 20
20867ad2antrr 730 . . . . . . . . . . . . . . . . . . . . 21
209 eluz 11161 . . . . . . . . . . . . . . . . . . . . 21
210191, 208, 209syl2anc 665 . . . . . . . . . . . . . . . . . . . 20
211207, 210mpbird 235 . . . . . . . . . . . . . . . . . . 19
212 uztrn 11164 . . . . . . . . . . . . . . . . . . 19
213211, 194, 212syl2anc 665 . . . . . . . . . . . . . . . . . 18
214 fzss2 11825 . . . . . . . . . . . . . . . . . 18
215213, 214syl 17 . . . . . . . . . . . . . . . . 17
216215sselda 3461 . . . . . . . . . . . . . . . 16
217166, 74sylan 473 . . . . . . . . . . . . . . . 16
218216, 217syldan 472 . . . . . . . . . . . . . . 15
219 seqcoll.c . . . . . . . . . . . . . . . 16
220166, 219sylan 473 . . . . . . . . . . . . . . 15
221172, 218, 220seqcl 12219 . . . . . . . . . . . . . 14
222 simplll 766 . . . . . . . . . . . . . . 15
223 elfzuz 11783 . . . . . . . . . . . . . . . . . 18
224 peano2uz 11201 . . . . . . . . . . . . . . . . . . 19
225172, 224syl 17 . . . . . . . . . . . . . . . . . 18
226 uztrn 11164 . . . . . . . . . . . . . . . . . 18
227223, 225, 226syl2anr 480 . . . . . . . . . . . . . . . . 17
228 elfzuz3 11784 . . . . . . . . . . . . . . . . . 18
229 uztrn 11164 . . . . . . . . . . . . . . . . . 18
230211, 228, 229syl2an 479 . . . . . . . . . . . . . . . . 17
231 elfzuzb 11781 . . . . . . . . . . . . . . . . 17
232227, 230, 231sylanbrc 668 . . . . . . . . . . . . . . . 16
233 elfzle1 11789 . . . . . . . . . . . . . . . . . . 19
234 elfzle2 11790 . . . . . . . . . . . . . . . . . . 19
235233, 234jca 534 . . . . . . . . . . . . . . . . . 18
236155ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . 22
237101ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24
238 simprr 764 . . . . . . . . . . . . . . . . . . . . . . . 24
239237, 238ffvelrnd 6029 . . . . . . . . . . . . . . . . . . . . . . 23
240 elfzelz 11787 . . . . . . . . . . . . . . . . . . . . . . 23
241239, 240syl 17 . . . . . . . . . . . . . . . . . . . . . 22
242 btwnnz 11001 . . . . . . . . . . . . . . . . . . . . . . . 24
2432423expib 1208 . . . . . . . . . . . . . . . . . . . . . . 23
244243con2d 118 . . . . . . . . . . . . . . . . . . . . . 22
245236, 241, 244sylc 62 . . . . . . . . . . . . . . . . . . . . 21
24635ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24
247162adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . 24
248 isorel 6223 . . . . . . . . . . . . . . . . . . . . . . . 24
249246, 247, 239, 248syl12anc 1262 . . . . . . . . . . . . . . . . . . . . . . 23
25037ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25
251250, 238, 113syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 24
252251breq2d 4429 . . . . . . . . . . . . . . . . . . . . . . 23
253182adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . 24
25434ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26
255254, 238sseldd 3462 . . . . . . . . . . . . . . . . . . . . . . . . 25
256 eluzelz 11157 . . . . . . . . . . . . . . . . . . . . . . . . 25
257255, 256syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
258 zltp1le 10975 . . . . . . . . . . . . . . . . . . . . . . . 24
259253, 257, 258syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23
260249, 252, 2593bitrd 282 . . . . . . . . . . . . . . . . . . . . . 22
261177adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . 24
262 isorel 6223 . . . . . . . . . . . . . . . . . . . . . . . 24
263246, 239, 261, 262syl12anc 1262 . . . . . . . . . . . . . . . . . . . . . . 23
264251breq1d 4427 . . . . . . . . . . . . . . . . . . . . . . 23
265186adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . 24
266 zltlem1 10978 . . . . . . . . . . . . . . . . . . . . . . . 24
267257, 265, 266syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23
268263, 264, 2673bitrd 282 . . . . . . . . . . . . . . . . . . . . . 22
269260, 268anbi12d 715 . . . . . . . . . . . . . . . . . . . . 21
270245, 269mtbid 301 . . . . . . . . . . . . . . . . . . . 20
271270expr 618 . . . . . . . . . . . . . . . . . . 19
272271con2d 118 . . . . . . . . . . . . . . . . . 18
273235, 272syl5 33 . . . . . . . . . . . . . . . . 17
274273imp 430 . . . . . . . . . . . . . . . 16
275232, 274eldifd 3444 . . . . . . . . . . . . . . 15
276222, 275, 126syl2anc 665 . . . . . . . . . . . . . 14
277168, 172, 194, 221, 276seqid2 12245 . . . . . . . . . . . . 13
278277oveq1d 6311 . . . . . . . . . . . 12
279 fveq2 5872 . . . . . . . . . . . . . . . . . 18
280 fveq2 5872 . . . . . . . . . . . . . . . . . . 19
281280fveq2d 5876 . . . . . . . . . . . . . . . . . 18
282279, 281eqeq12d 2442 . . . . . . . . . . . . . . . . 17
283282imbi2d 317 . . . . . . . . . . . . . . . 16
284283, 142vtoclga 3142 . . . . . . . . . . . . . . 15
285284impcom 431 . . . . . . . . . . . . . 14
286285adantlr 719 . . . . . . . . . . . . 13
287286oveq2d 6312 . . . . . . . . . . . 12
28894ad2antrr 730 . . . . . . . . . . . . 13
289186zcnd 11030 . . . . . . . . . . . . . . 15
290 ax-1cn 9586 . . . . . . . . . . . . . . 15
291 npcan 9873 . . . . . . . . . . . . . . 15
292289, 290, 291sylancl 666 . . . . . . . . . . . . . 14
293 uztrn 11164 . . . . . . . . . . . . . . . 16
294194, 172, 293syl2anc 665 . . . . . . . . . . . . . . 15
295 eluzp1p1 11173 . . . . . . . . . . . . . . 15
296294, 295syl 17 . . . . . . . . . . . . . 14
297292, 296eqeltrrd 2509 . . . . . . . . . . . . 13
298 seqm1 12216 . . . . . . . . . . . . 13
299288, 297, 298syl2anc 665 . . . . . . . . . . . 12
300278, 287, 2993eqtr4rd 2472 . . . . . . . . . . 11
301 seqp1 12214 . . . . . . . . . . . 12
302154, 301syl 17 . . . . . . . . . . 11
303300, 302eqeq12d 2442 . . . . . . . . . 10
304165, 303syl5ibr 224 . . . . . . . . 9
305304ex 435 . . . . . . . 8
306305a2d 29 . . . . . . 7
307164, 306syld 45 . . . . . 6
308307expcom 436 . . . . 5
309308a2d 29 . . . 4
31010, 17, 24, 31, 151, 309nnind 10616 . . 3
3113, 310mpcom 37 . 2
3121, 311mpd 15 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1867   cdif 3430   wss 3433   class class class wbr 4417  ccnv 4844   cres 4847  wf 5588  wf1o 5591  cfv 5592   wiso 5593  (class class class)co 6296  cc 9526  cr 9527  c1 9529   caddc 9531  cxr 9663   clt 9664   cle 9665   cmin 9849  cn 10598  cz 10926  cuz 11148  cfz 11771   cseq 12199  chash 12501 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-cnex 9584  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-isom 5601  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-er 7362  df-en 7569  df-dom 7570  df-sdom 7571  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-nn 10599  df-n0 10859  df-z 10927  df-uz 11149  df-fz 11772  df-seq 12200 This theorem is referenced by:  seqcoll2  12611  summolem2a  13748  prodmolem2a  13955
 Copyright terms: Public domain W3C validator