isercoll - Metamath Proof Explorer

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

Theorem isercoll 14398

Description: Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015.)

**Hypotheses**
Ref	Expression
isercoll.z
isercoll.m
isercoll.g
isercoll.i	$/\$
isercoll.0	$/\$ $\$
isercoll.f	$/\$
isercoll.h	$/\$

**Assertion**
Ref	Expression
isercoll

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem isercoll Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isercoll.z	. . . . . . . . . 10
2		uzssz 11707	. . . . . . . . . 10
3	1, 2	eqsstri 3635	. . . . . . . . 9
4		isercoll.g	. . . . . . . . . 10
5	4	ffvelrnda 6359	. . . . . . . . 9 $/\$
6	3, 5	sseldi 3601	. . . . . . . 8 $/\$
7		nnz 11399	. . . . . . . . . . . 12
8	7	ad2antlr 763	. . . . . . . . . . 11 $/\$ $/\$
9		fzfid 12772	. . . . . . . . . . . . 13 $/\$ $/\$
10		ffun 6048	. . . . . . . . . . . . . . . 16
11		funimacnv 5970	. . . . . . . . . . . . . . . 16
12	4, 10, 11	3syl 18	. . . . . . . . . . . . . . 15
13		inss1 3833	. . . . . . . . . . . . . . 15
14	12, 13	syl6eqss 3655	. . . . . . . . . . . . . 14
15	14	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$
16		ssfi 8180	. . . . . . . . . . . . 13 $/\$
17	9, 15, 16	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$
18		hashcl 13147	. . . . . . . . . . . 12
19		nn0z 11400	. . . . . . . . . . . 12
20	17, 18, 19	3syl 18	. . . . . . . . . . 11 $/\$ $/\$
21		ssid 3624	. . . . . . . . . . . . . . . . . . . 20
22		isercoll.m	. . . . . . . . . . . . . . . . . . . . 21
23		isercoll.i	. . . . . . . . . . . . . . . . . . . . 21 $/\$
24	1, 22, 4, 23	isercolllem1 14395	. . . . . . . . . . . . . . . . . . . 20 $/\$
25	21, 24	mpan2 707	. . . . . . . . . . . . . . . . . . 19
26		ffn 6045	. . . . . . . . . . . . . . . . . . . 20
27		fnresdm 6000	. . . . . . . . . . . . . . . . . . . 20
28		isoeq1 6567	. . . . . . . . . . . . . . . . . . . 20
29	4, 26, 27, 28	4syl 19	. . . . . . . . . . . . . . . . . . 19
30	25, 29	mpbid 222	. . . . . . . . . . . . . . . . . 18
31		isof1o 6573	. . . . . . . . . . . . . . . . . 18
32		f1ocnv 6149	. . . . . . . . . . . . . . . . . 18
33		f1ofun 6139	. . . . . . . . . . . . . . . . . 18
34	30, 31, 32, 33	4syl 19	. . . . . . . . . . . . . . . . 17
35		df-f1 5893	. . . . . . . . . . . . . . . . 17 $/\$
36	4, 34, 35	sylanbrc 698	. . . . . . . . . . . . . . . 16
37	36	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$
38		elfznn 12370	. . . . . . . . . . . . . . . 16
39	38	ssriv 3607	. . . . . . . . . . . . . . 15
40		ovex 6678	. . . . . . . . . . . . . . . 16
41	40	f1imaen 8018	. . . . . . . . . . . . . . 15 $/\$
42	37, 39, 41	sylancl 694	. . . . . . . . . . . . . 14 $/\$ $/\$
43		fzfid 12772	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44		enfii 8177	. . . . . . . . . . . . . . . 16 $/\$
45	43, 42, 44	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$
46		hashen 13135	. . . . . . . . . . . . . . 15 $/\$
47	45, 43, 46	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$
48	42, 47	mpbird 247	. . . . . . . . . . . . 13 $/\$ $/\$
49		nnnn0 11299	. . . . . . . . . . . . . . 15
50	49	ad2antlr 763	. . . . . . . . . . . . . 14 $/\$ $/\$
51		hashfz1 13134	. . . . . . . . . . . . . 14
52	50, 51	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
53	48, 52	eqtrd 2656	. . . . . . . . . . . 12 $/\$ $/\$
54	38	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
55		zssre 11384	. . . . . . . . . . . . . . . . . . . . . 22
56	3, 55	sstri 3612	. . . . . . . . . . . . . . . . . . . . 21
57	4	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
58		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
59	57, 38, 58	syl2an 494	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
60	56, 59	sseldi 3601	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
61	5	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
62	56, 61	sseldi 3601	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
63		eluzelz 11697	. . . . . . . . . . . . . . . . . . . . . 22
64	63	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
65	64	zred 11482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
66		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . 22
67	66	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
68	30	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
69		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
70		isorel 6576	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
71	68, 69, 54, 70	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
72	71	notbid 308	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
73	54	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
74	69	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
75	73, 74	lenltd 10183	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
76	60, 62	lenltd 10183	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
77	72, 75, 76	3bitr4d 300	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
78	67, 77	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
79		eluzle 11700	. . . . . . . . . . . . . . . . . . . . 21
80	79	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
81	60, 62, 65, 78, 80	letrd 10194	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
82	59, 1	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
83		elfz5 12334	. . . . . . . . . . . . . . . . . . . 20 $/\$
84	82, 64, 83	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
85	81, 84	mpbird 247	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
86	57, 26	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
87	86	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
88		elpreima 6337	. . . . . . . . . . . . . . . . . . 19 $/\$
89	87, 88	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
90	54, 85, 89	mpbir2and 957	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
91	90	ex 450	. . . . . . . . . . . . . . . 16 $/\$ $/\$
92	91	ssrdv 3609	. . . . . . . . . . . . . . 15 $/\$ $/\$
93		imass2 5501	. . . . . . . . . . . . . . 15
94	92, 93	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
95		ssdomg 8001	. . . . . . . . . . . . . 14
96	17, 94, 95	sylc 65	. . . . . . . . . . . . 13 $/\$ $/\$
97		hashdom 13168	. . . . . . . . . . . . . 14 $/\$
98	45, 17, 97	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$
99	96, 98	mpbird 247	. . . . . . . . . . . 12 $/\$ $/\$
100	53, 99	eqbrtrrd 4677	. . . . . . . . . . 11 $/\$ $/\$
101		eluz2 11693	. . . . . . . . . . 11 $/\$ $/\$
102	8, 20, 100, 101	syl3anbrc 1246	. . . . . . . . . 10 $/\$ $/\$
103		fveq2 6191	. . . . . . . . . . . . 13
104	103	eleq1d 2686	. . . . . . . . . . . 12
105	103	oveq1d 6665	. . . . . . . . . . . . . 14
106	105	fveq2d 6195	. . . . . . . . . . . . 13
107	106	breq1d 4663	. . . . . . . . . . . 12
108	104, 107	anbi12d 747	. . . . . . . . . . 11 $/\$ $/\$
109	108	rspcv 3305	. . . . . . . . . 10 $/\$ $/\$
110	102, 109	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
111	110	ralrimdva 2969	. . . . . . . 8 $/\$ $/\$ $/\$
112		fveq2 6191	. . . . . . . . . 10
113	112	raleqdv 3144	. . . . . . . . 9 $/\$ $/\$
114	113	rspcev 3309	. . . . . . . 8 $/\$ $/\$ $/\$
115	6, 111, 114	syl6an 568	. . . . . . 7 $/\$ $/\$ $/\$
116	115	rexlimdva 3031	. . . . . 6 $/\$ $/\$
117		1nn 11031	. . . . . . . . 9
118		ffvelrn 6357	. . . . . . . . 9 $/\$
119	4, 117, 118	sylancl 694	. . . . . . . 8
120	119, 1	syl6eleq 2711	. . . . . . 7
121		eluzelz 11697	. . . . . . 7
122		eqid 2622	. . . . . . . 8
123	122	rexuz3 14088	. . . . . . 7 $/\$ $/\$
124	120, 121, 123	3syl 18	. . . . . 6 $/\$ $/\$
125	116, 124	sylibrd 249	. . . . 5 $/\$ $/\$
126		fzfid 12772	. . . . . . . . 9 $/\$
127		funimacnv 5970	. . . . . . . . . . . 12
128	4, 10, 127	3syl 18	. . . . . . . . . . 11
129		inss1 3833	. . . . . . . . . . 11
130	128, 129	syl6eqss 3655	. . . . . . . . . 10
131	130	adantr 481	. . . . . . . . 9 $/\$
132		ssfi 8180	. . . . . . . . 9 $/\$
133	126, 131, 132	syl2anc 693	. . . . . . . 8 $/\$
134		hashcl 13147	. . . . . . . 8
135		nn0p1nn 11332	. . . . . . . 8
136	133, 134, 135	3syl 18	. . . . . . 7 $/\$
137		eluzle 11700	. . . . . . . . . . . . . . 15
138	137	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
139	133	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140		nn0z 11400	. . . . . . . . . . . . . . . 16
141	139, 134, 140	3syl 18	. . . . . . . . . . . . . . 15 $/\$ $/\$
142		eluzelz 11697	. . . . . . . . . . . . . . . 16
143	142	adantl 482	. . . . . . . . . . . . . . 15 $/\$ $/\$
144		zltp1le 11427	. . . . . . . . . . . . . . 15 $/\$
145	141, 143, 144	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$
146	138, 145	mpbird 247	. . . . . . . . . . . . 13 $/\$ $/\$
147		nn0re 11301	. . . . . . . . . . . . . . . 16
148	133, 134, 147	3syl 18	. . . . . . . . . . . . . . 15 $/\$
149	148	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$
150		eluznn 11758	. . . . . . . . . . . . . . . 16 $/\$
151	136, 150	sylan 488	. . . . . . . . . . . . . . 15 $/\$ $/\$
152	151	nnred 11035	. . . . . . . . . . . . . 14 $/\$ $/\$
153	149, 152	ltnled 10184	. . . . . . . . . . . . 13 $/\$ $/\$
154	146, 153	mpbid 222	. . . . . . . . . . . 12 $/\$ $/\$
155		fzss2 12381	. . . . . . . . . . . . . 14
156		imass2 5501	. . . . . . . . . . . . . 14
157		imass2 5501	. . . . . . . . . . . . . 14
158	155, 156, 157	3syl 18	. . . . . . . . . . . . 13
159		ssdomg 8001	. . . . . . . . . . . . . . 15
160	139, 159	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
161	4	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
162	161	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
163	162, 1	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
164	161, 151	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
165	3, 164	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
166	165	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
167		elfz5 12334	. . . . . . . . . . . . . . . . . . . . 21 $/\$
168	163, 166, 167	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
169	30	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
170		nnssre 11024	. . . . . . . . . . . . . . . . . . . . . . 23
171		ressxr 10083	. . . . . . . . . . . . . . . . . . . . . . 23
172	170, 171	sstri 3612	. . . . . . . . . . . . . . . . . . . . . 22
173	172	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
174		imassrn 5477	. . . . . . . . . . . . . . . . . . . . . . 23
175	161	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
176		frn 6053	. . . . . . . . . . . . . . . . . . . . . . . . 25
177	175, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
178	177, 56	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
179	174, 178	syl5ss 3614	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
180	179, 171	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
181		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
182	151	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
183		leisorel 13244	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
184	169, 173, 180, 181, 182, 183	syl122anc 1335	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
185	168, 184	bitr4d 271	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
186	185	pm5.32da 673	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
187		elpreima 6337	. . . . . . . . . . . . . . . . . . 19 $/\$
188	161, 26, 187	3syl 18	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
189		fznn 12408	. . . . . . . . . . . . . . . . . . 19 $/\$
190	143, 189	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
191	186, 188, 190	3bitr4d 300	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
192	191	eqrdv 2620	. . . . . . . . . . . . . . . 16 $/\$ $/\$
193	192	imaeq2d 5466	. . . . . . . . . . . . . . 15 $/\$ $/\$
194	193	sseq1d 3632	. . . . . . . . . . . . . 14 $/\$ $/\$
195	36	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
196		elfznn 12370	. . . . . . . . . . . . . . . . . . . 20
197	196	ssriv 3607	. . . . . . . . . . . . . . . . . . 19
198		ovex 6678	. . . . . . . . . . . . . . . . . . . 20
199	198	f1imaen 8018	. . . . . . . . . . . . . . . . . . 19 $/\$
200	195, 197, 199	sylancl 694	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
201		fzfid 12772	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
202		enfii 8177	. . . . . . . . . . . . . . . . . . . 20 $/\$
203	201, 200, 202	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
204		hashen 13135	. . . . . . . . . . . . . . . . . . 19 $/\$
205	203, 201, 204	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
206	200, 205	mpbird 247	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
207		nnnn0 11299	. . . . . . . . . . . . . . . . . 18
208		hashfz1 13134	. . . . . . . . . . . . . . . . . 18
209	151, 207, 208	3syl 18	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
210	206, 209	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$ $/\$
211	210	breq1d 4663	. . . . . . . . . . . . . . 15 $/\$ $/\$
212		hashdom 13168	. . . . . . . . . . . . . . . 16 $/\$
213	203, 139, 212	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$
214	211, 213	bitr3d 270	. . . . . . . . . . . . . 14 $/\$ $/\$
215	160, 194, 214	3imtr4d 283	. . . . . . . . . . . . 13 $/\$ $/\$
216	158, 215	syl5 34	. . . . . . . . . . . 12 $/\$ $/\$
217	154, 216	mtod 189	. . . . . . . . . . 11 $/\$ $/\$
218		eluzelz 11697	. . . . . . . . . . . . . 14
219	218	ad2antlr 763	. . . . . . . . . . . . 13 $/\$ $/\$
220		uztric 11709	. . . . . . . . . . . . 13 $/\$ $\/$
221	165, 219, 220	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
222	221	ord 392	. . . . . . . . . . 11 $/\$ $/\$
223	217, 222	mpd 15	. . . . . . . . . 10 $/\$ $/\$
224		oveq2 6658	. . . . . . . . . . . . . . . . 17
225	224	imaeq2d 5466	. . . . . . . . . . . . . . . 16
226	225	imaeq2d 5466	. . . . . . . . . . . . . . 15
227	226	fveq2d 6195	. . . . . . . . . . . . . 14
228	227	fveq2d 6195	. . . . . . . . . . . . 13
229	228	eleq1d 2686	. . . . . . . . . . . 12
230	228	oveq1d 6665	. . . . . . . . . . . . . 14
231	230	fveq2d 6195	. . . . . . . . . . . . 13
232	231	breq1d 4663	. . . . . . . . . . . 12
233	229, 232	anbi12d 747	. . . . . . . . . . 11 $/\$ $/\$
234	233	rspcv 3305	. . . . . . . . . 10 $/\$ $/\$
235	223, 234	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
236	193	fveq2d 6195	. . . . . . . . . . . . 13 $/\$ $/\$
237	236, 210	eqtrd 2656	. . . . . . . . . . . 12 $/\$ $/\$
238	237	fveq2d 6195	. . . . . . . . . . 11 $/\$ $/\$
239	238	eleq1d 2686	. . . . . . . . . 10 $/\$ $/\$
240	238	oveq1d 6665	. . . . . . . . . . . 12 $/\$ $/\$
241	240	fveq2d 6195	. . . . . . . . . . 11 $/\$ $/\$
242	241	breq1d 4663	. . . . . . . . . 10 $/\$ $/\$
243	239, 242	anbi12d 747	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
244	235, 243	sylibd 229	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
245	244	ralrimdva 2969	. . . . . . 7 $/\$ $/\$ $/\$
246		fveq2 6191	. . . . . . . . 9
247	246	raleqdv 3144	. . . . . . . 8 $/\$ $/\$
248	247	rspcev 3309	. . . . . . 7 $/\$ $/\$ $/\$
249	136, 245, 248	syl6an 568	. . . . . 6 $/\$ $/\$ $/\$
250	249	rexlimdva 3031	. . . . 5 $/\$ $/\$
251	125, 250	impbid 202	. . . 4 $/\$ $/\$
252	251	ralbidv 2986	. . 3 $/\$ $/\$
253	252	anbi2d 740	. 2 $/\$ $/\$ $/\$ $/\$
254		nnuz 11723	. . 3
255		1zzd 11408	. . 3
256		seqex 12803	. . . 4
257	256	a1i 11	. . 3
258		eqidd 2623	. . 3 $/\$
259	254, 255, 257, 258	clim2 14235	. 2 $/\$ $/\$
260	120, 121	syl 17	. . 3
261		seqex 12803	. . . 4
262	261	a1i 11	. . 3
263		isercoll.0	. . . 4 $/\$ $\$
264		isercoll.f	. . . 4 $/\$
265		isercoll.h	. . . 4 $/\$
266	1, 22, 4, 23, 263, 264, 265	isercolllem3 14397	. . 3 $/\$
267	122, 260, 262, 266	clim2 14235	. 2 $/\$ $/\$
268	253, 259, 267	3bitr4d 300	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990

wral 2912

wrex 2913

cvv 3200 $\$ cdif 3571

cin 3573

wss 3574 class class class wbr 4653

ccnv 5113

crn 5115

cres 5116

cima 5117

wfun 5882

wfn 5883

wf 5884

wf1 5885

wf1o 5887

cfv 5888

wiso 5889 (class class class)co 6650

cen 7952

cdom 7953

cfn 7955

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cxr 10073

clt 10074

cle 10075

cmin 10266

cn 11020

cn0 11292

cz 11377

cuz 11687

crp 11832

cfz 12326

cseq 12801

chash 13117

cabs 13974

cli 14215

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-seq 12802 df-hash 13118 df-clim 14219

This theorem is referenced by: isercoll2 14399

W3C validator