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

Theorem iseqcoll 10212
 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.)
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
iseqcoll
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem iseqcoll
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seqcoll.3 . 2
2 elfznn 9437 . . . 4
31, 2syl 14 . . 3
4 eleq1 2150 . . . . . 6
5 2fveq3 5294 . . . . . . 7
6 fveq2 5289 . . . . . . 7
75, 6eqeq12d 2102 . . . . . 6
84, 7imbi12d 232 . . . . 5
98imbi2d 228 . . . 4
10 eleq1 2150 . . . . . 6
11 2fveq3 5294 . . . . . . 7
12 fveq2 5289 . . . . . . 7
1311, 12eqeq12d 2102 . . . . . 6
1410, 13imbi12d 232 . . . . 5
1514imbi2d 228 . . . 4
16 eleq1 2150 . . . . . 6
17 2fveq3 5294 . . . . . . 7
18 fveq2 5289 . . . . . . 7
1917, 18eqeq12d 2102 . . . . . 6
2016, 19imbi12d 232 . . . . 5
2120imbi2d 228 . . . 4
22 eleq1 2150 . . . . . 6
23 2fveq3 5294 . . . . . . 7
24 fveq2 5289 . . . . . . 7
2523, 24eqeq12d 2102 . . . . . 6
2622, 25imbi12d 232 . . . . 5
2726imbi2d 228 . . . 4
28 seqcoll.1 . . . . . . . . 9
29 seqcoll.a . . . . . . . . 9
30 seqcoll.4 . . . . . . . . . 10
31 seqcoll.2 . . . . . . . . . . . . 13
32 isof1o 5568 . . . . . . . . . . . . 13
3331, 32syl 14 . . . . . . . . . . . 12
34 f1of 5237 . . . . . . . . . . . 12
3533, 34syl 14 . . . . . . . . . . 11
36 elfzuz2 9412 . . . . . . . . . . . . 13
371, 36syl 14 . . . . . . . . . . . 12
38 eluzfz1 9414 . . . . . . . . . . . 12
3937, 38syl 14 . . . . . . . . . . 11
4035, 39ffvelrnd 5419 . . . . . . . . . 10
4130, 40sseldd 3024 . . . . . . . . 9
42 eluzle 9000 . . . . . . . . . . . . 13
4337, 42syl 14 . . . . . . . . . . . 12
44 elfzelz 9409 . . . . . . . . . . . . . . . . 17
4544ssriv 3027 . . . . . . . . . . . . . . . 16
46 zssre 8727 . . . . . . . . . . . . . . . 16
4745, 46sstri 3032 . . . . . . . . . . . . . . 15
4847a1i 9 . . . . . . . . . . . . . 14
49 ressxr 7510 . . . . . . . . . . . . . 14
5048, 49syl6ss 3035 . . . . . . . . . . . . 13
51 eluzelre 8998 . . . . . . . . . . . . . . . 16
5251ssriv 3027 . . . . . . . . . . . . . . 15
5330, 52syl6ss 3035 . . . . . . . . . . . . . 14
5453, 49syl6ss 3035 . . . . . . . . . . . . 13
55 eluzfz2 9415 . . . . . . . . . . . . . 14
5637, 55syl 14 . . . . . . . . . . . . 13
57 leisorel 10207 . . . . . . . . . . . . 13
5831, 50, 54, 39, 56, 57syl122anc 1183 . . . . . . . . . . . 12
5943, 58mpbid 145 . . . . . . . . . . 11
6035, 56ffvelrnd 5419 . . . . . . . . . . . . . 14
6130, 60sseldd 3024 . . . . . . . . . . . . 13
62 eluzelz 8997 . . . . . . . . . . . . 13
6361, 62syl 14 . . . . . . . . . . . 12
64 elfz5 9401 . . . . . . . . . . . 12
6541, 63, 64syl2anc 403 . . . . . . . . . . 11
6659, 65mpbird 165 . . . . . . . . . 10
67 fveq2 5289 . . . . . . . . . . . . 13
6867eleq1d 2156 . . . . . . . . . . . 12
6968imbi2d 228 . . . . . . . . . . 11
70 elfzuz 9405 . . . . . . . . . . . 12
71 seqcoll.5 . . . . . . . . . . . . 13
7271expcom 114 . . . . . . . . . . . 12
7370, 72syl 14 . . . . . . . . . . 11
7469, 73vtoclga 2685 . . . . . . . . . 10
7566, 74mpcom 36 . . . . . . . . 9
76 eluzelz 8997 . . . . . . . . . . . . . . . . . 18
7741, 76syl 14 . . . . . . . . . . . . . . . . 17
78 peano2zm 8758 . . . . . . . . . . . . . . . . 17
7977, 78syl 14 . . . . . . . . . . . . . . . 16
8079zred 8838 . . . . . . . . . . . . . . 15
8177zred 8838 . . . . . . . . . . . . . . 15
8263zred 8838 . . . . . . . . . . . . . . 15
8381lem1d 8366 . . . . . . . . . . . . . . 15
8480, 81, 82, 83, 59letrd 7586 . . . . . . . . . . . . . 14
85 eluz 9001 . . . . . . . . . . . . . . 15
8679, 63, 85syl2anc 403 . . . . . . . . . . . . . 14
8784, 86mpbird 165 . . . . . . . . . . . . 13
88 fzss2 9446 . . . . . . . . . . . . 13
8987, 88syl 14 . . . . . . . . . . . 12
9089sselda 3023 . . . . . . . . . . 11
91 eluzel2 8993 . . . . . . . . . . . . . . 15
9241, 91syl 14 . . . . . . . . . . . . . 14
93 elfzm11 9472 . . . . . . . . . . . . . 14
9492, 77, 93syl2anc 403 . . . . . . . . . . . . 13
95 simp3 945 . . . . . . . . . . . . . 14
9681adantr 270 . . . . . . . . . . . . . . . . 17
9753sselda 3023 . . . . . . . . . . . . . . . . 17
98 f1ocnv 5250 . . . . . . . . . . . . . . . . . . . . . . . 24
9933, 98syl 14 . . . . . . . . . . . . . . . . . . . . . . 23
100 f1of 5237 . . . . . . . . . . . . . . . . . . . . . . 23
10199, 100syl 14 . . . . . . . . . . . . . . . . . . . . . 22
102101ffvelrnda 5418 . . . . . . . . . . . . . . . . . . . . 21
103 elfznn 9437 . . . . . . . . . . . . . . . . . . . . 21
104102, 103syl 14 . . . . . . . . . . . . . . . . . . . 20
105104nnge1d 8436 . . . . . . . . . . . . . . . . . . 19
10631adantr 270 . . . . . . . . . . . . . . . . . . . 20
10750adantr 270 . . . . . . . . . . . . . . . . . . . 20
10854adantr 270 . . . . . . . . . . . . . . . . . . . 20
10939adantr 270 . . . . . . . . . . . . . . . . . . . 20
110 leisorel 10207 . . . . . . . . . . . . . . . . . . . 20
111106, 107, 108, 109, 102, 110syl122anc 1183 . . . . . . . . . . . . . . . . . . 19
112105, 111mpbid 145 . . . . . . . . . . . . . . . . . 18
113 f1ocnvfv2 5539 . . . . . . . . . . . . . . . . . . 19
11433, 113sylan 277 . . . . . . . . . . . . . . . . . 18
115112, 114breqtrd 3861 . . . . . . . . . . . . . . . . 17
11696, 97, 115lensymd 7584 . . . . . . . . . . . . . . . 16
117116ex 113 . . . . . . . . . . . . . . 15
118117con2d 589 . . . . . . . . . . . . . 14
11995, 118syl5 32 . . . . . . . . . . . . 13
12094, 119sylbid 148 . . . . . . . . . . . 12
121120imp 122 . . . . . . . . . . 11
12290, 121eldifd 3007 . . . . . . . . . 10
123 seqcoll.6 . . . . . . . . . 10
124122, 123syldan 276 . . . . . . . . 9
125 seqcoll.c . . . . . . . . 9
12628, 29, 41, 75, 124, 71, 125iseqid 9904 . . . . . . . 8
127126fveq1d 5291 . . . . . . 7
128 uzid 9002 . . . . . . . . 9
12977, 128syl 14 . . . . . . . 8
130 fvres 5313 . . . . . . . 8
131129, 130syl 14 . . . . . . 7
13292adantr 270 . . . . . . . . . . 11
133 eluzelz 8997 . . . . . . . . . . . 12
134133adantl 271 . . . . . . . . . . 11
135132zred 8838 . . . . . . . . . . . 12
13681adantr 270 . . . . . . . . . . . 12
137134zred 8838 . . . . . . . . . . . 12
138 eluzle 9000 . . . . . . . . . . . . . 14
13941, 138syl 14 . . . . . . . . . . . . 13
140139adantr 270 . . . . . . . . . . . 12
141 eluzle 9000 . . . . . . . . . . . . 13
142141adantl 271 . . . . . . . . . . . 12
143135, 136, 137, 140, 142letrd 7586 . . . . . . . . . . 11
144 eluz2 8994 . . . . . . . . . . 11
145132, 134, 143, 144syl3anbrc 1127 . . . . . . . . . 10
146145, 71syldan 276 . . . . . . . . 9
14777, 146, 125iseq1 9840 . . . . . . . 8
148 fveq2 5289 . . . . . . . . . . . 12
149 2fveq3 5294 . . . . . . . . . . . 12
150148, 149eqeq12d 2102 . . . . . . . . . . 11
151150imbi2d 228 . . . . . . . . . 10
152 seqcoll.7 . . . . . . . . . . 11
153152expcom 114 . . . . . . . . . 10
154151, 153vtoclga 2685 . . . . . . . . 9
15539, 154mpcom 36 . . . . . . . 8
156147, 155eqtr4d 2123 . . . . . . 7
157127, 131, 1563eqtr3d 2128 . . . . . 6
158 1zzd 8747 . . . . . . 7
159 seqcoll.hcl . . . . . . 7
160158, 159, 125iseq1 9840 . . . . . 6
161157, 160eqtr4d 2123 . . . . 5
162161a1d 22 . . . 4
163 simplr 497 . . . . . . . . . . 11
164 nnuz 9023 . . . . . . . . . . 11
165163, 164syl6eleq 2180 . . . . . . . . . 10
166 nnz 8739 . . . . . . . . . . . 12
167166ad2antlr 473 . . . . . . . . . . 11
168 elfzuz3 9406 . . . . . . . . . . . 12
169168adantl 271 . . . . . . . . . . 11
170 peano2uzr 9042 . . . . . . . . . . 11
171167, 169, 170syl2anc 403 . . . . . . . . . 10
172 elfzuzb 9403 . . . . . . . . . 10
173165, 171, 172sylanbrc 408 . . . . . . . . 9
174173ex 113 . . . . . . . 8
175174imim1d 74 . . . . . . 7
176 oveq1 5641 . . . . . . . . . 10
177 simpll 496 . . . . . . . . . . . . . . 15
178 seqcoll.1b . . . . . . . . . . . . . . 15
179177, 178sylan 277 . . . . . . . . . . . . . 14
18030ad2antrr 472 . . . . . . . . . . . . . . 15
18135ad2antrr 472 . . . . . . . . . . . . . . . 16
182181, 173ffvelrnd 5419 . . . . . . . . . . . . . . 15
183180, 182sseldd 3024 . . . . . . . . . . . . . 14
184 nnre 8401 . . . . . . . . . . . . . . . . . . 19
185184ad2antlr 473 . . . . . . . . . . . . . . . . . 18
186185ltp1d 8363 . . . . . . . . . . . . . . . . 17
18731ad2antrr 472 . . . . . . . . . . . . . . . . . 18
188 simpr 108 . . . . . . . . . . . . . . . . . 18
189 isorel 5569 . . . . . . . . . . . . . . . . . 18
190187, 173, 188, 189syl12anc 1172 . . . . . . . . . . . . . . . . 17
191186, 190mpbid 145 . . . . . . . . . . . . . . . 16
192 eluzelz 8997 . . . . . . . . . . . . . . . . . 18
193183, 192syl 14 . . . . . . . . . . . . . . . . 17
194181, 188ffvelrnd 5419 . . . . . . . . . . . . . . . . . . 19
195180, 194sseldd 3024 . . . . . . . . . . . . . . . . . 18
196 eluzelz 8997 . . . . . . . . . . . . . . . . . 18
197195, 196syl 14 . . . . . . . . . . . . . . . . 17
198 zltlem1 8777 . . . . . . . . . . . . . . . . 17
199193, 197, 198syl2anc 403 . . . . . . . . . . . . . . . 16
200191, 199mpbid 145 . . . . . . . . . . . . . . 15
201 peano2zm 8758 . . . . . . . . . . . . . . . . 17
202197, 201syl 14 . . . . . . . . . . . . . . . 16
203 eluz 9001 . . . . . . . . . . . . . . . 16
204193, 202, 203syl2anc 403 . . . . . . . . . . . . . . 15
205200, 204mpbird 165 . . . . . . . . . . . . . 14
206177, 71sylan 277 . . . . . . . . . . . . . . 15
207177, 125sylan 277 . . . . . . . . . . . . . . 15
208183, 206, 207iseqcl 9846 . . . . . . . . . . . . . 14
209 simplll 500 . . . . . . . . . . . . . . 15
210 elfzuz 9405 . . . . . . . . . . . . . . . . . 18
211 peano2uz 9040 . . . . . . . . . . . . . . . . . . 19
212183, 211syl 14 . . . . . . . . . . . . . . . . . 18
213 uztrn 9004 . . . . . . . . . . . . . . . . . 18
214210, 212, 213syl2anr 284 . . . . . . . . . . . . . . . . 17
215202zred 8838 . . . . . . . . . . . . . . . . . . . 20
216197zred 8838 . . . . . . . . . . . . . . . . . . . 20
21782ad2antrr 472 . . . . . . . . . . . . . . . . . . . 20
218216lem1d 8366 . . . . . . . . . . . . . . . . . . . 20
219 elfzle2 9411 . . . . . . . . . . . . . . . . . . . . . 22
220219adantl 271 . . . . . . . . . . . . . . . . . . . . 21
22150ad2antrr 472 . . . . . . . . . . . . . . . . . . . . . 22
22254ad2antrr 472 . . . . . . . . . . . . . . . . . . . . . 22
22356ad2antrr 472 . . . . . . . . . . . . . . . . . . . . . 22
224 leisorel 10207 . . . . . . . . . . . . . . . . . . . . . 22
225187, 221, 222, 188, 223, 224syl122anc 1183 . . . . . . . . . . . . . . . . . . . . 21
226220, 225mpbid 145 . . . . . . . . . . . . . . . . . . . 20
227215, 216, 217, 218, 226letrd 7586 . . . . . . . . . . . . . . . . . . 19
22863ad2antrr 472 . . . . . . . . . . . . . . . . . . . 20
229 eluz 9001 . . . . . . . . . . . . . . . . . . . 20
230202, 228, 229syl2anc 403 . . . . . . . . . . . . . . . . . . 19
231227, 230mpbird 165 . . . . . . . . . . . . . . . . . 18
232 elfzuz3 9406 . . . . . . . . . . . . . . . . . 18
233 uztrn 9004 . . . . . . . . . . . . . . . . . 18
234231, 232, 233syl2an 283 . . . . . . . . . . . . . . . . 17
235 elfzuzb 9403 . . . . . . . . . . . . . . . . 17
236214, 234, 235sylanbrc 408 . . . . . . . . . . . . . . . 16
237166ad2antlr 473 . . . . . . . . . . . . . . . . . . . . 21
238101ad2antrr 472 . . . . . . . . . . . . . . . . . . . . . . 23
239 simprr 499 . . . . . . . . . . . . . . . . . . . . . . 23
240238, 239ffvelrnd 5419 . . . . . . . . . . . . . . . . . . . . . 22
241 elfzelz 9409 . . . . . . . . . . . . . . . . . . . . . 22
242240, 241syl 14 . . . . . . . . . . . . . . . . . . . . 21
243 btwnnz 8810 . . . . . . . . . . . . . . . . . . . . . . 23
2442433expib 1146 . . . . . . . . . . . . . . . . . . . . . 22
245244con2d 589 . . . . . . . . . . . . . . . . . . . . 21
246237, 242, 245sylc 61 . . . . . . . . . . . . . . . . . . . 20
24731ad2antrr 472 . . . . . . . . . . . . . . . . . . . . . . 23
248173adantrr 463 . . . . . . . . . . . . . . . . . . . . . . 23
249 isorel 5569 . . . . . . . . . . . . . . . . . . . . . . 23
250247, 248, 240, 249syl12anc 1172 . . . . . . . . . . . . . . . . . . . . . 22
25133ad2antrr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
252251, 239, 113syl2anc 403 . . . . . . . . . . . . . . . . . . . . . . 23
253252breq2d 3849 . . . . . . . . . . . . . . . . . . . . . 22
254193adantrr 463 . . . . . . . . . . . . . . . . . . . . . . 23
25530ad2antrr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
256255, 239sseldd 3024 . . . . . . . . . . . . . . . . . . . . . . . 24
257 eluzelz 8997 . . . . . . . . . . . . . . . . . . . . . . . 24
258256, 257syl 14 . . . . . . . . . . . . . . . . . . . . . . 23
259 zltp1le 8774 . . . . . . . . . . . . . . . . . . . . . . 23
260254, 258, 259syl2anc 403 . . . . . . . . . . . . . . . . . . . . . 22
261250, 253, 2603bitrd 212 . . . . . . . . . . . . . . . . . . . . 21
262188adantrr 463 . . . . . . . . . . . . . . . . . . . . . . 23
263 isorel 5569 . . . . . . . . . . . . . . . . . . . . . . 23
264247, 240, 262, 263syl12anc 1172 . . . . . . . . . . . . . . . . . . . . . 22
265252breq1d 3847 . . . . . . . . . . . . . . . . . . . . . 22
266197adantrr 463 . . . . . . . . . . . . . . . . . . . . . . 23
267 zltlem1 8777 . . . . . . . . . . . . . . . . . . . . . . 23
268258, 266, 267syl2anc 403 . . . . . . . . . . . . . . . . . . . . . 22
269264, 265, 2683bitrd 212 . . . . . . . . . . . . . . . . . . . . 21
270261, 269anbi12d 457 . . . . . . . . . . . . . . . . . . . 20
271246, 270mtbid 632 . . . . . . . . . . . . . . . . . . 19
272271expr 367 . . . . . . . . . . . . . . . . . 18
273272con2d 589 . . . . . . . . . . . . . . . . 17
274 elfzle1 9410 . . . . . . . . . . . . . . . . . 18
275 elfzle2 9411 . . . . . . . . . . . . . . . . . 18
276274, 275jca 300 . . . . . . . . . . . . . . . . 17
277273, 276impel 274 . . . . . . . . . . . . . . . 16
278236, 277eldifd 3007 . . . . . . . . . . . . . . 15
279209, 278, 123syl2anc 403 . . . . . . . . . . . . . 14
280179, 183, 205, 208, 279, 206, 207iseqid2 9906 . . . . . . . . . . . . 13
281280oveq1d 5649 . . . . . . . . . . . 12
282 fveq2 5289 . . . . . . . . . . . . . . . . . 18
283 2fveq3 5294 . . . . . . . . . . . . . . . . . 18
284282, 283eqeq12d 2102 . . . . . . . . . . . . . . . . 17
285284imbi2d 228 . . . . . . . . . . . . . . . 16
286285, 153vtoclga 2685 . . . . . . . . . . . . . . 15
287286impcom 123 . . . . . . . . . . . . . 14
288287adantlr 461 . . . . . . . . . . . . 13
289288oveq2d 5650 . . . . . . . . . . . 12
29092ad2antrr 472 . . . . . . . . . . . . 13
291197zcnd 8839 . . . . . . . . . . . . . . 15
292 ax-1cn 7417 . . . . . . . . . . . . . . 15
293 npcan 7670 . . . . . . . . . . . . . . 15
294291, 292, 293sylancl 404 . . . . . . . . . . . . . 14
295 uztrn 9004 . . . . . . . . . . . . . . . 16
296205, 183, 295syl2anc 403 . . . . . . . . . . . . . . 15
297 eluzp1p1 9013 . . . . . . . . . . . . . . 15
298296, 297syl 14 . . . . . . . . . . . . . 14
299294, 298eqeltrrd 2165 . . . . . . . . . . . . 13
300290, 299, 206, 207iseqm1 9853 . . . . . . . . . . . 12
301281, 289, 3003eqtr4rd 2131 . . . . . . . . . . 11
302177, 159sylan 277 . . . . . . . . . . . 12
303165, 302, 207iseqp1 9847 . . . . . . . . . . 11
304301, 303eqeq12d 2102 . . . . . . . . . 10
305176, 304syl5ibr 154 . . . . . . . . 9
306305ex 113 . . . . . . . 8
307306a2d 26 . . . . . . 7
308175, 307syld 44 . . . . . 6
309308expcom 114 . . . . 5
310309a2d 26 . . . 4
3119, 15, 21, 27, 162, 310nnind 8410 . . 3
3123, 311mpcom 36 . 2
3131, 312mpd 13 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 102   wb 103   w3a 924   wceq 1289   wcel 1438   cdif 2994   wss 2997   class class class wbr 3837  ccnv 4427   cres 4430  wf 4998  wf1o 5001  cfv 5002   wiso 5003  (class class class)co 5634  cc 7327  cr 7328  c1 7330   caddc 7332  cxr 7500   clt 7501   cle 7502   cmin 7632  cn 8394  cz 8720  cuz 8988  cfz 9393   cseq4 9816  ♯chash 10148 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3946  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027  ax-un 4251  ax-setind 4343  ax-iinf 4393  ax-cnex 7415  ax-resscn 7416  ax-1cn 7417  ax-1re 7418  ax-icn 7419  ax-addcl 7420  ax-addrcl 7421  ax-mulcl 7422  ax-addcom 7424  ax-addass 7426  ax-distr 7428  ax-i2m1 7429  ax-0lt1 7430  ax-0id 7432  ax-rnegex 7433  ax-cnre 7435  ax-pre-ltirr 7436  ax-pre-ltwlin 7437  ax-pre-lttrn 7438  ax-pre-ltadd 7440 This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-int 3684  df-iun 3727  df-br 3838  df-opab 3892  df-mpt 3893  df-tr 3929  df-id 4111  df-iord 4184  df-on 4186  df-ilim 4187  df-suc 4189  df-iom 4396  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009  df-fv 5010  df-isom 5011  df-riota 5590  df-ov 5637  df-oprab 5638  df-mpt2 5639  df-1st 5893  df-2nd 5894  df-recs 6052  df-frec 6138  df-pnf 7503  df-mnf 7504  df-xr 7505  df-ltxr 7506  df-le 7507  df-sub 7634  df-neg 7635  df-inn 8395  df-n0 8644  df-z 8721  df-uz 8989  df-fz 9394  df-fzo 9519  df-iseq 9818 This theorem is referenced by:  isummolem2a  10735
 Copyright terms: Public domain W3C validator