Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  seq3coll Unicode version

Theorem seq3coll 10597
 Description: The function contains a sparse set of nonzero values to be summed. The function is an order isomorphism from the set of nonzero values of to a 1-based finite sequence, and collects these nonzero 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.) (Revised by Jim Kingdon, 9-Apr-2023.)
Hypotheses
Ref Expression
seqcoll.1
seqcoll.1b
seqcoll.c
seqcoll.a
seqcoll.2
seqcoll.3
seqcoll.4
seqcoll.5
seqcoll.hcl
seqcoll.6
seqcoll.7
Assertion
Ref Expression
seq3coll
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem seq3coll
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seqcoll.3 . 2
2 elfznn 9846 . . . 4
31, 2syl 14 . . 3
4 eleq1 2202 . . . . . 6
5 2fveq3 5426 . . . . . . 7
6 fveq2 5421 . . . . . . 7
75, 6eqeq12d 2154 . . . . . 6
84, 7imbi12d 233 . . . . 5
98imbi2d 229 . . . 4
10 eleq1 2202 . . . . . 6
11 2fveq3 5426 . . . . . . 7
12 fveq2 5421 . . . . . . 7
1311, 12eqeq12d 2154 . . . . . 6
1410, 13imbi12d 233 . . . . 5
1514imbi2d 229 . . . 4
16 eleq1 2202 . . . . . 6
17 2fveq3 5426 . . . . . . 7
18 fveq2 5421 . . . . . . 7
1917, 18eqeq12d 2154 . . . . . 6
2016, 19imbi12d 233 . . . . 5
2120imbi2d 229 . . . 4
22 eleq1 2202 . . . . . 6
23 2fveq3 5426 . . . . . . 7
24 fveq2 5421 . . . . . . 7
2523, 24eqeq12d 2154 . . . . . 6
2622, 25imbi12d 233 . . . . 5
2726imbi2d 229 . . . 4
28 seqcoll.1 . . . . . . . . 9
29 seqcoll.a . . . . . . . . 9
30 seqcoll.4 . . . . . . . . . 10
31 seqcoll.2 . . . . . . . . . . . . 13
32 isof1o 5708 . . . . . . . . . . . . 13
3331, 32syl 14 . . . . . . . . . . . 12
34 f1of 5367 . . . . . . . . . . . 12
3533, 34syl 14 . . . . . . . . . . 11
36 elfzuz2 9821 . . . . . . . . . . . . 13
371, 36syl 14 . . . . . . . . . . . 12
38 eluzfz1 9823 . . . . . . . . . . . 12
3937, 38syl 14 . . . . . . . . . . 11
4035, 39ffvelrnd 5556 . . . . . . . . . 10
4130, 40sseldd 3098 . . . . . . . . 9
42 eluzle 9350 . . . . . . . . . . . . 13
4337, 42syl 14 . . . . . . . . . . . 12
44 elfzelz 9818 . . . . . . . . . . . . . . . . 17
4544ssriv 3101 . . . . . . . . . . . . . . . 16
46 zssre 9073 . . . . . . . . . . . . . . . 16
4745, 46sstri 3106 . . . . . . . . . . . . . . 15
4847a1i 9 . . . . . . . . . . . . . 14
49 ressxr 7821 . . . . . . . . . . . . . 14
5048, 49sstrdi 3109 . . . . . . . . . . . . 13
51 eluzelre 9348 . . . . . . . . . . . . . . . 16
5251ssriv 3101 . . . . . . . . . . . . . . 15
5330, 52sstrdi 3109 . . . . . . . . . . . . . 14
5453, 49sstrdi 3109 . . . . . . . . . . . . 13
55 eluzfz2 9824 . . . . . . . . . . . . . 14
5637, 55syl 14 . . . . . . . . . . . . 13
57 leisorel 10592 . . . . . . . . . . . . 13
5831, 50, 54, 39, 56, 57syl122anc 1225 . . . . . . . . . . . 12
5943, 58mpbid 146 . . . . . . . . . . 11
6035, 56ffvelrnd 5556 . . . . . . . . . . . . . 14
6130, 60sseldd 3098 . . . . . . . . . . . . 13
62 eluzelz 9347 . . . . . . . . . . . . 13
6361, 62syl 14 . . . . . . . . . . . 12
64 elfz5 9810 . . . . . . . . . . . 12
6541, 63, 64syl2anc 408 . . . . . . . . . . 11
6659, 65mpbird 166 . . . . . . . . . 10
67 fveq2 5421 . . . . . . . . . . . . 13
6867eleq1d 2208 . . . . . . . . . . . 12
6968imbi2d 229 . . . . . . . . . . 11
70 elfzuz 9814 . . . . . . . . . . . 12
71 seqcoll.5 . . . . . . . . . . . . 13
7271expcom 115 . . . . . . . . . . . 12
7370, 72syl 14 . . . . . . . . . . 11
7469, 73vtoclga 2752 . . . . . . . . . 10
7566, 74mpcom 36 . . . . . . . . 9
76 eluzelz 9347 . . . . . . . . . . . . . . . . . 18
7741, 76syl 14 . . . . . . . . . . . . . . . . 17
78 peano2zm 9104 . . . . . . . . . . . . . . . . 17
7977, 78syl 14 . . . . . . . . . . . . . . . 16
8079zred 9185 . . . . . . . . . . . . . . 15
8177zred 9185 . . . . . . . . . . . . . . 15
8263zred 9185 . . . . . . . . . . . . . . 15
8381lem1d 8703 . . . . . . . . . . . . . . 15
8480, 81, 82, 83, 59letrd 7898 . . . . . . . . . . . . . 14
85 eluz 9351 . . . . . . . . . . . . . . 15
8679, 63, 85syl2anc 408 . . . . . . . . . . . . . 14
8784, 86mpbird 166 . . . . . . . . . . . . 13
88 fzss2 9856 . . . . . . . . . . . . 13
8987, 88syl 14 . . . . . . . . . . . 12
9089sselda 3097 . . . . . . . . . . 11
91 eluzel2 9343 . . . . . . . . . . . . . . 15
9241, 91syl 14 . . . . . . . . . . . . . 14
93 elfzm11 9883 . . . . . . . . . . . . . 14
9492, 77, 93syl2anc 408 . . . . . . . . . . . . 13
95 simp3 983 . . . . . . . . . . . . . 14
9681adantr 274 . . . . . . . . . . . . . . . . 17
9753sselda 3097 . . . . . . . . . . . . . . . . 17
98 f1ocnv 5380 . . . . . . . . . . . . . . . . . . . . . . . 24
9933, 98syl 14 . . . . . . . . . . . . . . . . . . . . . . 23
100 f1of 5367 . . . . . . . . . . . . . . . . . . . . . . 23
10199, 100syl 14 . . . . . . . . . . . . . . . . . . . . . 22
102101ffvelrnda 5555 . . . . . . . . . . . . . . . . . . . . 21
103 elfznn 9846 . . . . . . . . . . . . . . . . . . . . 21
104102, 103syl 14 . . . . . . . . . . . . . . . . . . . 20
105104nnge1d 8775 . . . . . . . . . . . . . . . . . . 19
10631adantr 274 . . . . . . . . . . . . . . . . . . . 20
10750adantr 274 . . . . . . . . . . . . . . . . . . . 20
10854adantr 274 . . . . . . . . . . . . . . . . . . . 20
10939adantr 274 . . . . . . . . . . . . . . . . . . . 20
110 leisorel 10592 . . . . . . . . . . . . . . . . . . . 20
111106, 107, 108, 109, 102, 110syl122anc 1225 . . . . . . . . . . . . . . . . . . 19
112105, 111mpbid 146 . . . . . . . . . . . . . . . . . 18
113 f1ocnvfv2 5679 . . . . . . . . . . . . . . . . . . 19
11433, 113sylan 281 . . . . . . . . . . . . . . . . . 18
115112, 114breqtrd 3954 . . . . . . . . . . . . . . . . 17
11696, 97, 115lensymd 7896 . . . . . . . . . . . . . . . 16
117116ex 114 . . . . . . . . . . . . . . 15
118117con2d 613 . . . . . . . . . . . . . 14
11995, 118syl5 32 . . . . . . . . . . . . 13
12094, 119sylbid 149 . . . . . . . . . . . 12
121120imp 123 . . . . . . . . . . 11
12290, 121eldifd 3081 . . . . . . . . . 10
123 seqcoll.6 . . . . . . . . . 10
124122, 123syldan 280 . . . . . . . . 9
125 seqcoll.c . . . . . . . . 9
12628, 29, 41, 75, 124, 71, 125seq3id 10293 . . . . . . . 8
127126fveq1d 5423 . . . . . . 7
128 uzid 9352 . . . . . . . . 9
12977, 128syl 14 . . . . . . . 8
130 fvres 5445 . . . . . . . 8
131129, 130syl 14 . . . . . . 7
13292adantr 274 . . . . . . . . . . 11
133 eluzelz 9347 . . . . . . . . . . . 12
134133adantl 275 . . . . . . . . . . 11
135132zred 9185 . . . . . . . . . . . 12
13681adantr 274 . . . . . . . . . . . 12
137134zred 9185 . . . . . . . . . . . 12
138 eluzle 9350 . . . . . . . . . . . . . 14
13941, 138syl 14 . . . . . . . . . . . . 13
140139adantr 274 . . . . . . . . . . . 12
141 eluzle 9350 . . . . . . . . . . . . 13
142141adantl 275 . . . . . . . . . . . 12
143135, 136, 137, 140, 142letrd 7898 . . . . . . . . . . 11
144 eluz2 9344 . . . . . . . . . . 11
145132, 134, 143, 144syl3anbrc 1165 . . . . . . . . . 10
146145, 71syldan 280 . . . . . . . . 9
14777, 146, 125seq3-1 10245 . . . . . . . 8
148 fveq2 5421 . . . . . . . . . . . 12
149 2fveq3 5426 . . . . . . . . . . . 12
150148, 149eqeq12d 2154 . . . . . . . . . . 11
151150imbi2d 229 . . . . . . . . . 10
152 seqcoll.7 . . . . . . . . . . 11
153152expcom 115 . . . . . . . . . 10
154151, 153vtoclga 2752 . . . . . . . . 9
15539, 154mpcom 36 . . . . . . . 8
156147, 155eqtr4d 2175 . . . . . . 7
157127, 131, 1563eqtr3d 2180 . . . . . 6
158 1zzd 9093 . . . . . . 7
159 seqcoll.hcl . . . . . . 7
160158, 159, 125seq3-1 10245 . . . . . 6
161157, 160eqtr4d 2175 . . . . 5
162161a1d 22 . . . 4
163 simplr 519 . . . . . . . . . . 11
164 nnuz 9373 . . . . . . . . . . 11
165163, 164eleqtrdi 2232 . . . . . . . . . 10
166 nnz 9085 . . . . . . . . . . . 12
167166ad2antlr 480 . . . . . . . . . . 11
168 elfzuz3 9815 . . . . . . . . . . . 12
169168adantl 275 . . . . . . . . . . 11
170 peano2uzr 9392 . . . . . . . . . . 11
171167, 169, 170syl2anc 408 . . . . . . . . . 10
172 elfzuzb 9812 . . . . . . . . . 10
173165, 171, 172sylanbrc 413 . . . . . . . . 9
174173ex 114 . . . . . . . 8
175174imim1d 75 . . . . . . 7
176 oveq1 5781 . . . . . . . . . 10
177 simpll 518 . . . . . . . . . . . . . . 15
178 seqcoll.1b . . . . . . . . . . . . . . 15
179177, 178sylan 281 . . . . . . . . . . . . . 14
18030ad2antrr 479 . . . . . . . . . . . . . . 15
18135ad2antrr 479 . . . . . . . . . . . . . . . 16
182181, 173ffvelrnd 5556 . . . . . . . . . . . . . . 15
183180, 182sseldd 3098 . . . . . . . . . . . . . 14
184 nnre 8739 . . . . . . . . . . . . . . . . . . 19
185184ad2antlr 480 . . . . . . . . . . . . . . . . . 18
186185ltp1d 8700 . . . . . . . . . . . . . . . . 17
18731ad2antrr 479 . . . . . . . . . . . . . . . . . 18
188 simpr 109 . . . . . . . . . . . . . . . . . 18
189 isorel 5709 . . . . . . . . . . . . . . . . . 18
190187, 173, 188, 189syl12anc 1214 . . . . . . . . . . . . . . . . 17
191186, 190mpbid 146 . . . . . . . . . . . . . . . 16
192 eluzelz 9347 . . . . . . . . . . . . . . . . . 18
193183, 192syl 14 . . . . . . . . . . . . . . . . 17
194181, 188ffvelrnd 5556 . . . . . . . . . . . . . . . . . . 19
195180, 194sseldd 3098 . . . . . . . . . . . . . . . . . 18
196 eluzelz 9347 . . . . . . . . . . . . . . . . . 18
197195, 196syl 14 . . . . . . . . . . . . . . . . 17
198 zltlem1 9123 . . . . . . . . . . . . . . . . 17
199193, 197, 198syl2anc 408 . . . . . . . . . . . . . . . 16
200191, 199mpbid 146 . . . . . . . . . . . . . . 15
201 peano2zm 9104 . . . . . . . . . . . . . . . . 17
202197, 201syl 14 . . . . . . . . . . . . . . . 16
203 eluz 9351 . . . . . . . . . . . . . . . 16
204193, 202, 203syl2anc 408 . . . . . . . . . . . . . . 15
205200, 204mpbird 166 . . . . . . . . . . . . . 14
206 eqid 2139 . . . . . . . . . . . . . . . 16
20792ad2antrr 479 . . . . . . . . . . . . . . . 16
208177, 71sylan 281 . . . . . . . . . . . . . . . 16
209177, 125sylan 281 . . . . . . . . . . . . . . . 16
210206, 207, 208, 209seqf 10246 . . . . . . . . . . . . . . 15
211210, 183ffvelrnd 5556 . . . . . . . . . . . . . 14
212 simplll 522 . . . . . . . . . . . . . . 15
213 elfzuz 9814 . . . . . . . . . . . . . . . . . 18
214 peano2uz 9390 . . . . . . . . . . . . . . . . . . 19
215183, 214syl 14 . . . . . . . . . . . . . . . . . 18
216 uztrn 9354 . . . . . . . . . . . . . . . . . 18
217213, 215, 216syl2anr 288 . . . . . . . . . . . . . . . . 17
218202zred 9185 . . . . . . . . . . . . . . . . . . . 20
219197zred 9185 . . . . . . . . . . . . . . . . . . . 20
22082ad2antrr 479 . . . . . . . . . . . . . . . . . . . 20
221219lem1d 8703 . . . . . . . . . . . . . . . . . . . 20
222 elfzle2 9820 . . . . . . . . . . . . . . . . . . . . . 22
223222adantl 275 . . . . . . . . . . . . . . . . . . . . 21
22450ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . 22
22554ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . 22
22656ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . 22
227 leisorel 10592 . . . . . . . . . . . . . . . . . . . . . 22
228187, 224, 225, 188, 226, 227syl122anc 1225 . . . . . . . . . . . . . . . . . . . . 21
229223, 228mpbid 146 . . . . . . . . . . . . . . . . . . . 20
230218, 219, 220, 221, 229letrd 7898 . . . . . . . . . . . . . . . . . . 19
23163ad2antrr 479 . . . . . . . . . . . . . . . . . . . 20
232 eluz 9351 . . . . . . . . . . . . . . . . . . . 20
233202, 231, 232syl2anc 408 . . . . . . . . . . . . . . . . . . 19
234230, 233mpbird 166 . . . . . . . . . . . . . . . . . 18
235 elfzuz3 9815 . . . . . . . . . . . . . . . . . 18
236 uztrn 9354 . . . . . . . . . . . . . . . . . 18
237234, 235, 236syl2an 287 . . . . . . . . . . . . . . . . 17
238 elfzuzb 9812 . . . . . . . . . . . . . . . . 17
239217, 237, 238sylanbrc 413 . . . . . . . . . . . . . . . 16
240166ad2antlr 480 . . . . . . . . . . . . . . . . . . . . 21
241101ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . 23
242 simprr 521 . . . . . . . . . . . . . . . . . . . . . . 23
243241, 242ffvelrnd 5556 . . . . . . . . . . . . . . . . . . . . . 22
244 elfzelz 9818 . . . . . . . . . . . . . . . . . . . . . 22
245243, 244syl 14 . . . . . . . . . . . . . . . . . . . . 21
246 btwnnz 9157 . . . . . . . . . . . . . . . . . . . . . . 23
2472463expib 1184 . . . . . . . . . . . . . . . . . . . . . 22
248247con2d 613 . . . . . . . . . . . . . . . . . . . . 21
249240, 245, 248sylc 62 . . . . . . . . . . . . . . . . . . . 20
25031ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . 23
251173adantrr 470 . . . . . . . . . . . . . . . . . . . . . . 23
252 isorel 5709 . . . . . . . . . . . . . . . . . . . . . . 23
253250, 251, 243, 252syl12anc 1214 . . . . . . . . . . . . . . . . . . . . . 22
25433ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . . 24
255254, 242, 113syl2anc 408 . . . . . . . . . . . . . . . . . . . . . . 23
256255breq2d 3941 . . . . . . . . . . . . . . . . . . . . . 22
257193adantrr 470 . . . . . . . . . . . . . . . . . . . . . . 23
25830ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25
259258, 242sseldd 3098 . . . . . . . . . . . . . . . . . . . . . . . 24
260 eluzelz 9347 . . . . . . . . . . . . . . . . . . . . . . . 24
261259, 260syl 14 . . . . . . . . . . . . . . . . . . . . . . 23
262 zltp1le 9120 . . . . . . . . . . . . . . . . . . . . . . 23
263257, 261, 262syl2anc 408 . . . . . . . . . . . . . . . . . . . . . 22
264253, 256, 2633bitrd 213 . . . . . . . . . . . . . . . . . . . . 21
265188adantrr 470 . . . . . . . . . . . . . . . . . . . . . . 23
266 isorel 5709 . . . . . . . . . . . . . . . . . . . . . . 23
267250, 243, 265, 266syl12anc 1214 . . . . . . . . . . . . . . . . . . . . . 22
268255breq1d 3939 . . . . . . . . . . . . . . . . . . . . . 22
269197adantrr 470 . . . . . . . . . . . . . . . . . . . . . . 23
270 zltlem1 9123 . . . . . . . . . . . . . . . . . . . . . . 23
271261, 269, 270syl2anc 408 . . . . . . . . . . . . . . . . . . . . . 22
272267, 268, 2713bitrd 213 . . . . . . . . . . . . . . . . . . . . 21
273264, 272anbi12d 464 . . . . . . . . . . . . . . . . . . . 20
274249, 273mtbid 661 . . . . . . . . . . . . . . . . . . 19
275274expr 372 . . . . . . . . . . . . . . . . . 18
276275con2d 613 . . . . . . . . . . . . . . . . 17
277 elfzle1 9819 . . . . . . . . . . . . . . . . . 18
278 elfzle2 9820 . . . . . . . . . . . . . . . . . 18
279277, 278jca 304 . . . . . . . . . . . . . . . . 17
280276, 279impel 278 . . . . . . . . . . . . . . . 16
281239, 280eldifd 3081 . . . . . . . . . . . . . . 15
282212, 281, 123syl2anc 408 . . . . . . . . . . . . . 14
283179, 183, 205, 211, 282, 208, 209seq3id2 10294 . . . . . . . . . . . . 13
284283oveq1d 5789 . . . . . . . . . . . 12
285 fveq2 5421 . . . . . . . . . . . . . . . . . 18
286 2fveq3 5426 . . . . . . . . . . . . . . . . . 18
287285, 286eqeq12d 2154 . . . . . . . . . . . . . . . . 17
288287imbi2d 229 . . . . . . . . . . . . . . . 16
289288, 153vtoclga 2752 . . . . . . . . . . . . . . 15
290289impcom 124 . . . . . . . . . . . . . 14
291290adantlr 468 . . . . . . . . . . . . 13
292291oveq2d 5790 . . . . . . . . . . . 12
293197zcnd 9186 . . . . . . . . . . . . . . 15
294 ax-1cn 7725 . . . . . . . . . . . . . . 15
295 npcan 7983 . . . . . . . . . . . . . . 15
296293, 294, 295sylancl 409 . . . . . . . . . . . . . 14
297 uztrn 9354 . . . . . . . . . . . . . . . 16
298205, 183, 297syl2anc 408 . . . . . . . . . . . . . . 15
299 eluzp1p1 9363 . . . . . . . . . . . . . . 15
300298, 299syl 14 . . . . . . . . . . . . . 14
301296, 300eqeltrrd 2217 . . . . . . . . . . . . 13
302207, 301, 208, 209seq3m1 10253 . . . . . . . . . . . 12
303284, 292, 3023eqtr4rd 2183 . . . . . . . . . . 11
304177, 159sylan 281 . . . . . . . . . . . 12
305165, 304, 209seq3p1 10247 . . . . . . . . . . 11
306303, 305eqeq12d 2154 . . . . . . . . . 10
307176, 306syl5ibr 155 . . . . . . . . 9
308307ex 114 . . . . . . . 8
309308a2d 26 . . . . . . 7
310175, 309syld 45 . . . . . 6
311310expcom 115 . . . . 5
312311a2d 26 . . . 4
3139, 15, 21, 27, 162, 312nnind 8748 . . 3
3143, 313mpcom 36 . 2
3151, 314mpd 13 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wb 104   w3a 962   wceq 1331   wcel 1480   cdif 3068   wss 3071   class class class wbr 3929  ccnv 4538   cres 4541  wf 5119  wf1o 5122  cfv 5123   wiso 5124  (class class class)co 5774  cc 7630  cr 7631  c1 7633   caddc 7635  cxr 7811   clt 7812   cle 7813   cmin 7945  cn 8732  cz 9066  cuz 9338  cfz 9802   cseq 10230  ♯chash 10533 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7723  ax-resscn 7724  ax-1cn 7725  ax-1re 7726  ax-icn 7727  ax-addcl 7728  ax-addrcl 7729  ax-mulcl 7730  ax-addcom 7732  ax-addass 7734  ax-distr 7736  ax-i2m1 7737  ax-0lt1 7738  ax-0id 7740  ax-rnegex 7741  ax-cnre 7743  ax-pre-ltirr 7744  ax-pre-ltwlin 7745  ax-pre-lttrn 7746  ax-pre-ltadd 7748 This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-pnf 7814  df-mnf 7815  df-xr 7816  df-ltxr 7817  df-le 7818  df-sub 7947  df-neg 7948  df-inn 8733  df-n0 8990  df-z 9067  df-uz 9339  df-fz 9803  df-fzo 9932  df-seqfrec 10231 This theorem is referenced by:  summodclem2a  11162  prodmodclem2a  11357
 Copyright terms: Public domain W3C validator