Theorem isercoll 13490

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:   ,,   ,,   ,,   ,,   ,,   ,M,   ,

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 11129	. . . . . . . . . 10
3	1, 2	eqsstri 3533	. . . . . . . . 9
4		isercoll.g	. . . . . . . . . 10
5	4	ffvelrnda 6031	. . . . . . . . 9
6	3, 5	sseldi 3501	. . . . . . . 8
7		nnz 10911	. . . . . . . . . . . 12
8	7	ad2antlr 726	. . . . . . . . . . 11
9		fzfid 12083	. . . . . . . . . . . . 13
10		ffun 5738	. . . . . . . . . . . . . . . 16
11		funimacnv 5665	. . . . . . . . . . . . . . . 16
12	4, 10, 11	3syl 20	. . . . . . . . . . . . . . 15
13		inss1 3717	. . . . . . . . . . . . . . 15
14	12, 13	syl6eqss 3553	. . . . . . . . . . . . . 14
15	14	ad2antrr 725	. . . . . . . . . . . . 13
16		ssfi 7760	. . . . . . . . . . . . 13
17	9, 15, 16	syl2anc 661	. . . . . . . . . . . 12
18		hashcl 12428	. . . . . . . . . . . 12
19		nn0z 10912	. . . . . . . . . . . 12
20	17, 18, 19	3syl 20	. . . . . . . . . . 11
21		ssid 3522	. . . . . . . . . . . . . . . . . . . 20
22		isercoll.m	. . . . . . . . . . . . . . . . . . . . 21
23		isercoll.i	. . . . . . . . . . . . . . . . . . . . 21
24	1, 22, 4, 23	isercolllem1 13487	. . . . . . . . . . . . . . . . . . . 20
25	21, 24	mpan2 671	. . . . . . . . . . . . . . . . . . 19
26		ffn 5736	. . . . . . . . . . . . . . . . . . . 20
27		fnresdm 5695	. . . . . . . . . . . . . . . . . . . 20
28		isoeq1 6215	. . . . . . . . . . . . . . . . . . . 20
29	4, 26, 27, 28	4syl 21	. . . . . . . . . . . . . . . . . . 19
30	25, 29	mpbid 210	. . . . . . . . . . . . . . . . . 18
31		isof1o 6221	. . . . . . . . . . . . . . . . . 18
32		f1ocnv 5833	. . . . . . . . . . . . . . . . . 18
33		f1ofun 5823	. . . . . . . . . . . . . . . . . 18
34	30, 31, 32, 33	4syl 21	. . . . . . . . . . . . . . . . 17
35		df-f1 5598	. . . . . . . . . . . . . . . . 17
36	4, 34, 35	sylanbrc 664	. . . . . . . . . . . . . . . 16
37	36	ad2antrr 725	. . . . . . . . . . . . . . 15
38		elfznn 11743	. . . . . . . . . . . . . . . 16
39	38	ssriv 3507	. . . . . . . . . . . . . . 15
40		ovex 6324	. . . . . . . . . . . . . . . 16
41	40	f1imaen 7597	. . . . . . . . . . . . . . 15
42	37, 39, 41	sylancl 662	. . . . . . . . . . . . . 14
43		fzfid 12083	. . . . . . . . . . . . . . . 16
44		enfii 7757	. . . . . . . . . . . . . . . 16
45	43, 42, 44	syl2anc 661	. . . . . . . . . . . . . . 15
46		hashen 12420	. . . . . . . . . . . . . . 15
47	45, 43, 46	syl2anc 661	. . . . . . . . . . . . . 14
48	42, 47	mpbird 232	. . . . . . . . . . . . 13
49		nnnn0 10827	. . . . . . . . . . . . . . 15
50	49	ad2antlr 726	. . . . . . . . . . . . . 14
51		hashfz1 12419	. . . . . . . . . . . . . 14
52	50, 51	syl 16	. . . . . . . . . . . . 13
53	48, 52	eqtrd 2498	. . . . . . . . . . . 12
54	38	adantl 466	. . . . . . . . . . . . . . . . . 18
55		zssre 10896	. . . . . . . . . . . . . . . . . . . . . 22
56	3, 55	sstri 3512	. . . . . . . . . . . . . . . . . . . . 21
57	4	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22
58		ffvelrn 6029	. . . . . . . . . . . . . . . . . . . . . 22
59	57, 38, 58	syl2an 477	. . . . . . . . . . . . . . . . . . . . 21
60	56, 59	sseldi 3501	. . . . . . . . . . . . . . . . . . . 20
61	5	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21
62	56, 61	sseldi 3501	. . . . . . . . . . . . . . . . . . . 20
63		eluzelz 11119	. . . . . . . . . . . . . . . . . . . . . 22
64	63	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . 21
65	64	zred 10994	. . . . . . . . . . . . . . . . . . . 20
66		elfzle2 11719	. . . . . . . . . . . . . . . . . . . . . 22
67	66	adantl 466	. . . . . . . . . . . . . . . . . . . . 21
68	30	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . 24
69		simpllr 760	. . . . . . . . . . . . . . . . . . . . . . . 24
70		isorel 6222	. . . . . . . . . . . . . . . . . . . . . . . 24
71	68, 69, 54, 70	syl12anc 1226	. . . . . . . . . . . . . . . . . . . . . . 23
72	71	notbid 294	. . . . . . . . . . . . . . . . . . . . . 22
73	54	nnred 10576	. . . . . . . . . . . . . . . . . . . . . . 23
74	69	nnred 10576	. . . . . . . . . . . . . . . . . . . . . . 23
75	73, 74	lenltd 9752	. . . . . . . . . . . . . . . . . . . . . 22
76	60, 62	lenltd 9752	. . . . . . . . . . . . . . . . . . . . . 22
77	72, 75, 76	3bitr4d 285	. . . . . . . . . . . . . . . . . . . . 21
78	67, 77	mpbid 210	. . . . . . . . . . . . . . . . . . . 20
79		eluzle 11122	. . . . . . . . . . . . . . . . . . . . 21
80	79	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20
81	60, 62, 65, 78, 80	letrd 9760	. . . . . . . . . . . . . . . . . . 19
82	59, 1	syl6eleq 2555	. . . . . . . . . . . . . . . . . . . 20
83		elfz5 11709	. . . . . . . . . . . . . . . . . . . 20
84	82, 64, 83	syl2anc 661	. . . . . . . . . . . . . . . . . . 19
85	81, 84	mpbird 232	. . . . . . . . . . . . . . . . . 18
86	57, 26	syl 16	. . . . . . . . . . . . . . . . . . . 20
87	86	adantr 465	. . . . . . . . . . . . . . . . . . 19
88		elpreima 6007	. . . . . . . . . . . . . . . . . . 19
89	87, 88	syl 16	. . . . . . . . . . . . . . . . . 18
90	54, 85, 89	mpbir2and 922	. . . . . . . . . . . . . . . . 17
91	90	ex 434	. . . . . . . . . . . . . . . 16
92	91	ssrdv 3509	. . . . . . . . . . . . . . 15
93		imass2 5377	. . . . . . . . . . . . . . 15
94	92, 93	syl 16	. . . . . . . . . . . . . 14
95		ssdomg 7581	. . . . . . . . . . . . . 14
96	17, 94, 95	sylc 60	. . . . . . . . . . . . 13
97		hashdom 12447	. . . . . . . . . . . . . 14
98	45, 17, 97	syl2anc 661	. . . . . . . . . . . . 13
99	96, 98	mpbird 232	. . . . . . . . . . . 12
100	53, 99	eqbrtrrd 4474	. . . . . . . . . . 11
101		eluz2 11116	. . . . . . . . . . 11
102	8, 20, 100, 101	syl3anbrc 1180	. . . . . . . . . 10
103		fveq2 5871	. . . . . . . . . . . . 13
104	103	eleq1d 2526	. . . . . . . . . . . 12
105	103	oveq1d 6311	. . . . . . . . . . . . . 14
106	105	fveq2d 5875	. . . . . . . . . . . . 13
107	106	breq1d 4462	. . . . . . . . . . . 12
108	104, 107	anbi12d 710	. . . . . . . . . . 11
109	108	rspcv 3206	. . . . . . . . . 10
110	102, 109	syl 16	. . . . . . . . 9
111	110	ralrimdva 2875	. . . . . . . 8
112		fveq2 5871	. . . . . . . . . 10
113	112	raleqdv 3060	. . . . . . . . 9
114	113	rspcev 3210	. . . . . . . 8
115	6, 111, 114	syl6an 545	. . . . . . 7
116	115	rexlimdva 2949	. . . . . 6
117		1nn 10572	. . . . . . . . 9
118		ffvelrn 6029	. . . . . . . . 9
119	4, 117, 118	sylancl 662	. . . . . . . 8
120	119, 1	syl6eleq 2555	. . . . . . 7
121		eluzelz 11119	. . . . . . 7
122		eqid 2457	. . . . . . . 8
123	122	rexuz3 13181	. . . . . . 7
124	120, 121, 123	3syl 20	. . . . . 6
125	116, 124	sylibrd 234	. . . . 5
126		fzfid 12083	. . . . . . . . 9
127		funimacnv 5665	. . . . . . . . . . . 12
128	4, 10, 127	3syl 20	. . . . . . . . . . 11
129		inss1 3717	. . . . . . . . . . 11
130	128, 129	syl6eqss 3553	. . . . . . . . . 10
131	130	adantr 465	. . . . . . . . 9
132		ssfi 7760	. . . . . . . . 9
133	126, 131, 132	syl2anc 661	. . . . . . . 8
134		hashcl 12428	. . . . . . . 8
135		nn0p1nn 10860	. . . . . . . 8
136	133, 134, 135	3syl 20	. . . . . . 7
137		eluzle 11122	. . . . . . . . . . . . . . 15
138	137	adantl 466	. . . . . . . . . . . . . 14
139	133	adantr 465	. . . . . . . . . . . . . . . 16
140		nn0z 10912	. . . . . . . . . . . . . . . 16
141	139, 134, 140	3syl 20	. . . . . . . . . . . . . . 15
142		eluzelz 11119	. . . . . . . . . . . . . . . 16
143	142	adantl 466	. . . . . . . . . . . . . . 15
144		zltp1le 10938	. . . . . . . . . . . . . . 15
145	141, 143, 144	syl2anc 661	. . . . . . . . . . . . . 14
146	138, 145	mpbird 232	. . . . . . . . . . . . 13
147		nn0re 10829	. . . . . . . . . . . . . . . 16
148	133, 134, 147	3syl 20	. . . . . . . . . . . . . . 15
149	148	adantr 465	. . . . . . . . . . . . . 14
150		eluznn 11181	. . . . . . . . . . . . . . . 16
151	136, 150	sylan 471	. . . . . . . . . . . . . . 15
152	151	nnred 10576	. . . . . . . . . . . . . 14
153	149, 152	ltnled 9753	. . . . . . . . . . . . 13
154	146, 153	mpbid 210	. . . . . . . . . . . 12
155		fzss2 11752	. . . . . . . . . . . . . 14
156		imass2 5377	. . . . . . . . . . . . . 14
157		imass2 5377	. . . . . . . . . . . . . 14
158	155, 156, 157	3syl 20	. . . . . . . . . . . . 13
159		ssdomg 7581	. . . . . . . . . . . . . . 15
160	139, 159	syl 16	. . . . . . . . . . . . . 14
161	4	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23
162	161	ffvelrnda 6031	. . . . . . . . . . . . . . . . . . . . . 22
163	162, 1	syl6eleq 2555	. . . . . . . . . . . . . . . . . . . . 21
164	161, 151	ffvelrnd 6032	. . . . . . . . . . . . . . . . . . . . . . 23
165	3, 164	sseldi 3501	. . . . . . . . . . . . . . . . . . . . . 22
166	165	adantr 465	. . . . . . . . . . . . . . . . . . . . 21
167		elfz5 11709	. . . . . . . . . . . . . . . . . . . . 21
168	163, 166, 167	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20
169	30	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21
170		nnssre 10565	. . . . . . . . . . . . . . . . . . . . . . 23
171		ressxr 9658	. . . . . . . . . . . . . . . . . . . . . . 23
172	170, 171	sstri 3512	. . . . . . . . . . . . . . . . . . . . . 22
173	172	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
174		imassrn 5353	. . . . . . . . . . . . . . . . . . . . . . 23
175	161	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25
176		frn 5742	. . . . . . . . . . . . . . . . . . . . . . . . 25
177	175, 176	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24
178	177, 56	syl6ss 3515	. . . . . . . . . . . . . . . . . . . . . . 23
179	174, 178	syl5ss 3514	. . . . . . . . . . . . . . . . . . . . . 22
180	179, 171	syl6ss 3515	. . . . . . . . . . . . . . . . . . . . 21
181		simpr 461	. . . . . . . . . . . . . . . . . . . . 21
182	151	adantr 465	. . . . . . . . . . . . . . . . . . . . 21
183		leisorel 12509	. . . . . . . . . . . . . . . . . . . . 21
184	169, 173, 180, 181, 182, 183	syl122anc 1237	. . . . . . . . . . . . . . . . . . . 20
185	168, 184	bitr4d 256	. . . . . . . . . . . . . . . . . . 19
186	185	pm5.32da 641	. . . . . . . . . . . . . . . . . 18
187		elpreima 6007	. . . . . . . . . . . . . . . . . . 19
188	161, 26, 187	3syl 20	. . . . . . . . . . . . . . . . . 18
189		fznn 11776	. . . . . . . . . . . . . . . . . . 19
190	143, 189	syl 16	. . . . . . . . . . . . . . . . . 18
191	186, 188, 190	3bitr4d 285	. . . . . . . . . . . . . . . . 17
192	191	eqrdv 2454	. . . . . . . . . . . . . . . 16
193	192	imaeq2d 5342	. . . . . . . . . . . . . . 15
194	193	sseq1d 3530	. . . . . . . . . . . . . 14
195	36	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19
196		elfznn 11743	. . . . . . . . . . . . . . . . . . . 20
197	196	ssriv 3507	. . . . . . . . . . . . . . . . . . 19
198		ovex 6324	. . . . . . . . . . . . . . . . . . . 20
199	198	f1imaen 7597	. . . . . . . . . . . . . . . . . . 19
200	195, 197, 199	sylancl 662	. . . . . . . . . . . . . . . . . 18
201		fzfid 12083	. . . . . . . . . . . . . . . . . . . 20
202		enfii 7757	. . . . . . . . . . . . . . . . . . . 20
203	201, 200, 202	syl2anc 661	. . . . . . . . . . . . . . . . . . 19
204		hashen 12420	. . . . . . . . . . . . . . . . . . 19
205	203, 201, 204	syl2anc 661	. . . . . . . . . . . . . . . . . 18
206	200, 205	mpbird 232	. . . . . . . . . . . . . . . . 17
207		nnnn0 10827	. . . . . . . . . . . . . . . . . 18
208		hashfz1 12419	. . . . . . . . . . . . . . . . . 18
209	151, 207, 208	3syl 20	. . . . . . . . . . . . . . . . 17
210	206, 209	eqtrd 2498	. . . . . . . . . . . . . . . 16
211	210	breq1d 4462	. . . . . . . . . . . . . . 15
212		hashdom 12447	. . . . . . . . . . . . . . . 16
213	203, 139, 212	syl2anc 661	. . . . . . . . . . . . . . 15
214	211, 213	bitr3d 255	. . . . . . . . . . . . . 14
215	160, 194, 214	3imtr4d 268	. . . . . . . . . . . . 13
216	158, 215	syl5 32	. . . . . . . . . . . 12
217	154, 216	mtod 177	. . . . . . . . . . 11
218		eluzelz 11119	. . . . . . . . . . . . . 14
219	218	ad2antlr 726	. . . . . . . . . . . . 13
220		uztric 11131	. . . . . . . . . . . . 13
221	165, 219, 220	syl2anc 661	. . . . . . . . . . . 12
222	221	ord 377	. . . . . . . . . . 11
223	217, 222	mpd 15	. . . . . . . . . 10
224		oveq2 6304	. . . . . . . . . . . . . . . . 17
225	224	imaeq2d 5342	. . . . . . . . . . . . . . . 16
226	225	imaeq2d 5342	. . . . . . . . . . . . . . 15
227	226	fveq2d 5875	. . . . . . . . . . . . . 14
228	227	fveq2d 5875	. . . . . . . . . . . . 13
229	228	eleq1d 2526	. . . . . . . . . . . 12
230	228	oveq1d 6311	. . . . . . . . . . . . . 14
231	230	fveq2d 5875	. . . . . . . . . . . . 13
232	231	breq1d 4462	. . . . . . . . . . . 12
233	229, 232	anbi12d 710	. . . . . . . . . . 11
234	233	rspcv 3206	. . . . . . . . . 10
235	223, 234	syl 16	. . . . . . . . 9
236	193	fveq2d 5875	. . . . . . . . . . . . 13
237	236, 210	eqtrd 2498	. . . . . . . . . . . 12
238	237	fveq2d 5875	. . . . . . . . . . 11
239	238	eleq1d 2526	. . . . . . . . . 10
240	238	oveq1d 6311	. . . . . . . . . . . 12
241	240	fveq2d 5875	. . . . . . . . . . 11
242	241	breq1d 4462	. . . . . . . . . 10
243	239, 242	anbi12d 710	. . . . . . . . 9
244	235, 243	sylibd 214	. . . . . . . 8
245	244	ralrimdva 2875	. . . . . . 7
246		fveq2 5871	. . . . . . . . 9
247	246	raleqdv 3060	. . . . . . . 8
248	247	rspcev 3210	. . . . . . 7
249	136, 245, 248	syl6an 545	. . . . . 6
250	249	rexlimdva 2949	. . . . 5
251	125, 250	impbid 191	. . . 4
252	251	ralbidv 2896	. . 3
253	252	anbi2d 703	. 2
254		nnuz 11145	. . 3
255		1zzd 10920	. . 3
256		seqex 12109	. . . 4
257	256	a1i 11	. . 3
258		eqidd 2458	. . 3
259	254, 255, 257, 258	clim2 13327	. 2
260	120, 121	syl 16	. . 3
261		seqex 12109	. . . 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 13489	. . 3
267	122, 260, 262, 266	clim2 13327	. 2
268	253, 259, 267	3bitr4d 285	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  E.wrex 2808  cvv 3109  \cdif 3472  i^icin 3474  C_wss 3475   class class class wbr 4452  `'ccnv 5003  rancrn 5005  |`cres 5006  "cima 5007  Funwfun 5587  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590  -1-1-onto->wf1o 5592  `cfv 5593  Isomwiso 5594  (class class class)co 6296  cen 7533  cdom 7534  cfn 7536  cc 9511  cr 9512  0cc0 9513  1c1 9514  caddc 9516  cxr 9648  clt 9649  cle 9650  cmin 9828  cn 10561  cn0 10820  cz 10889  cuz 11110  crp 11249  cfz 11701  seqcseq 12107  chash 12405  cabs 13067  cli 13307

This theorem is referenced by:  isercoll2  13491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-inf2 8079  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590  ax-pre-sup 9591

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-recs 7061  df-rdg 7095  df-1o 7149  df-oadd 7153  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  df-sup 7921  df-card 8341  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-nn 10562  df-n0 10821  df-z 10890  df-uz 11111  df-fz 11702  df-seq 12108  df-hash 12406  df-clim 13311