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

Theorem isercoll 12512
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,   ,
Allowed substitution hint:   ( )

Proof of Theorem isercoll
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isercoll.z . . . . . . . . . 10
2 uzssz 10556 . . . . . . . . . 10
31, 2eqsstri 3367 . . . . . . . . 9
4 isercoll.g . . . . . . . . . 10
54ffvelrnda 5918 . . . . . . . . 9
63, 5sseldi 3335 . . . . . . . 8
7 nnz 10354 . . . . . . . . . . . 12
87ad2antlr 709 . . . . . . . . . . 11
9 fzfid 11363 . . . . . . . . . . . . 13
10 ffun 5640 . . . . . . . . . . . . . . . 16
11 funimacnv 5572 . . . . . . . . . . . . . . . 16
124, 10, 113syl 19 . . . . . . . . . . . . . . 15
13 inss1 3549 . . . . . . . . . . . . . . 15
1412, 13syl6eqss 3387 . . . . . . . . . . . . . 14
1514ad2antrr 708 . . . . . . . . . . . . 13
16 ssfi 7378 . . . . . . . . . . . . 13
179, 15, 16syl2anc 644 . . . . . . . . . . . 12
18 hashcl 11690 . . . . . . . . . . . 12
19 nn0z 10355 . . . . . . . . . . . 12
2017, 18, 193syl 19 . . . . . . . . . . 11
21 ssid 3356 . . . . . . . . . . . . . . . . . . . 20
22 isercoll.m . . . . . . . . . . . . . . . . . . . . 21
23 isercoll.i . . . . . . . . . . . . . . . . . . . . 21
241, 22, 4, 23isercolllem1 12509 . . . . . . . . . . . . . . . . . . . 20
2521, 24mpan2 654 . . . . . . . . . . . . . . . . . . 19
26 ffn 5638 . . . . . . . . . . . . . . . . . . . 20
27 fnresdm 5601 . . . . . . . . . . . . . . . . . . . 20
28 isoeq1 6087 . . . . . . . . . . . . . . . . . . . 20
294, 26, 27, 284syl 20 . . . . . . . . . . . . . . . . . . 19
3025, 29mpbid 203 . . . . . . . . . . . . . . . . . 18
31 isof1o 6093 . . . . . . . . . . . . . . . . . 18
32 f1ocnv 5734 . . . . . . . . . . . . . . . . . 18
33 f1ofun 5723 . . . . . . . . . . . . . . . . . 18
3430, 31, 32, 334syl 20 . . . . . . . . . . . . . . . . 17
35 df-f1 5506 . . . . . . . . . . . . . . . . 17
364, 34, 35sylanbrc 647 . . . . . . . . . . . . . . . 16
3736ad2antrr 708 . . . . . . . . . . . . . . 15
38 elfznn 11131 . . . . . . . . . . . . . . . 16
3938ssriv 3341 . . . . . . . . . . . . . . 15
40 ovex 6154 . . . . . . . . . . . . . . . 16
4140f1imaen 7218 . . . . . . . . . . . . . . 15
4237, 39, 41sylancl 645 . . . . . . . . . . . . . 14
43 fzfid 11363 . . . . . . . . . . . . . . . 16
44 enfii 7375 . . . . . . . . . . . . . . . 16
4543, 42, 44syl2anc 644 . . . . . . . . . . . . . . 15
46 hashen 11682 . . . . . . . . . . . . . . 15
4745, 43, 46syl2anc 644 . . . . . . . . . . . . . 14
4842, 47mpbird 225 . . . . . . . . . . . . 13
49 nnnn0 10279 . . . . . . . . . . . . . . 15
5049ad2antlr 709 . . . . . . . . . . . . . 14
51 hashfz1 11681 . . . . . . . . . . . . . 14
5250, 51syl 16 . . . . . . . . . . . . 13
5348, 52eqtrd 2475 . . . . . . . . . . . 12
5438adantl 454 . . . . . . . . . . . . . . . . . 18
55 zssre 10340 . . . . . . . . . . . . . . . . . . . . . 22
563, 55sstri 3346 . . . . . . . . . . . . . . . . . . . . 21
574ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22
58 ffvelrn 5916 . . . . . . . . . . . . . . . . . . . . . 22
5957, 38, 58syl2an 465 . . . . . . . . . . . . . . . . . . . . 21
6056, 59sseldi 3335 . . . . . . . . . . . . . . . . . . . 20
615ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21
6256, 61sseldi 3335 . . . . . . . . . . . . . . . . . . . 20
63 eluzelz 10547 . . . . . . . . . . . . . . . . . . . . . 22
6463ad2antlr 709 . . . . . . . . . . . . . . . . . . . . 21
6564zred 10426 . . . . . . . . . . . . . . . . . . . 20
66 elfzle2 11112 . . . . . . . . . . . . . . . . . . . . . 22
6766adantl 454 . . . . . . . . . . . . . . . . . . . . 21
6830ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . 24
69 simpllr 737 . . . . . . . . . . . . . . . . . . . . . . . 24
70 isorel 6094 . . . . . . . . . . . . . . . . . . . . . . . 24
7168, 69, 54, 70syl12anc 1183 . . . . . . . . . . . . . . . . . . . . . . 23
7271notbid 287 . . . . . . . . . . . . . . . . . . . . . 22
7354nnred 10066 . . . . . . . . . . . . . . . . . . . . . . 23
7469nnred 10066 . . . . . . . . . . . . . . . . . . . . . . 23
7573, 74lenltd 9270 . . . . . . . . . . . . . . . . . . . . . 22
7660, 62lenltd 9270 . . . . . . . . . . . . . . . . . . . . . 22
7772, 75, 763bitr4d 278 . . . . . . . . . . . . . . . . . . . . 21
7867, 77mpbid 203 . . . . . . . . . . . . . . . . . . . 20
79 eluzle 10549 . . . . . . . . . . . . . . . . . . . . 21
8079ad2antlr 709 . . . . . . . . . . . . . . . . . . . 20
8160, 62, 65, 78, 80letrd 9278 . . . . . . . . . . . . . . . . . . 19
8259, 1syl6eleq 2533 . . . . . . . . . . . . . . . . . . . 20
83 elfz5 11102 . . . . . . . . . . . . . . . . . . . 20
8482, 64, 83syl2anc 644 . . . . . . . . . . . . . . . . . . 19
8581, 84mpbird 225 . . . . . . . . . . . . . . . . . 18
8657, 26syl 16 . . . . . . . . . . . . . . . . . . . 20
8786adantr 453 . . . . . . . . . . . . . . . . . . 19
88 elpreima 5898 . . . . . . . . . . . . . . . . . . 19
8987, 88syl 16 . . . . . . . . . . . . . . . . . 18
9054, 85, 89mpbir2and 890 . . . . . . . . . . . . . . . . 17
9190ex 425 . . . . . . . . . . . . . . . 16
9291ssrdv 3343 . . . . . . . . . . . . . . 15
93 imass2 5284 . . . . . . . . . . . . . . 15
9492, 93syl 16 . . . . . . . . . . . . . 14
95 ssdomg 7202 . . . . . . . . . . . . . 14
9617, 94, 95sylc 59 . . . . . . . . . . . . 13
97 hashdom 11704 . . . . . . . . . . . . . 14
9845, 17, 97syl2anc 644 . . . . . . . . . . . . 13
9996, 98mpbird 225 . . . . . . . . . . . 12
10053, 99eqbrtrrd 4265 . . . . . . . . . . 11
101 eluz2 10545 . . . . . . . . . . 11
1028, 20, 100, 101syl3anbrc 1139 . . . . . . . . . 10
103 fveq2 5775 . . . . . . . . . . . . 13
104103eleq1d 2509 . . . . . . . . . . . 12
105103oveq1d 6144 . . . . . . . . . . . . . 14
106105fveq2d 5779 . . . . . . . . . . . . 13
107106breq1d 4253 . . . . . . . . . . . 12
108104, 107anbi12d 693 . . . . . . . . . . 11
109108rspcv 3057 . . . . . . . . . 10
110102, 109syl 16 . . . . . . . . 9
111110ralrimdva 2803 . . . . . . . 8
112 fveq2 5775 . . . . . . . . . 10
113112raleqdv 2917 . . . . . . . . 9
114113rspcev 3061 . . . . . . . 8
1156, 111, 114ee12an 1373 . . . . . . 7
116115rexlimdva 2837 . . . . . 6
117 1nn 10062 . . . . . . . . 9
118 ffvelrn 5916 . . . . . . . . 9
1194, 117, 118sylancl 645 . . . . . . . 8
120119, 1syl6eleq 2533 . . . . . . 7
121 eluzelz 10547 . . . . . . 7
122 eqid 2443 . . . . . . . 8
123122rexuz3 12203 . . . . . . 7
124120, 121, 1233syl 19 . . . . . 6
125116, 124sylibrd 227 . . . . 5
126 fzfid 11363 . . . . . . . . 9
127 funimacnv 5572 . . . . . . . . . . . 12
1284, 10, 1273syl 19 . . . . . . . . . . 11
129 inss1 3549 . . . . . . . . . . 11
130128, 129syl6eqss 3387 . . . . . . . . . 10
131130adantr 453 . . . . . . . . 9
132 ssfi 7378 . . . . . . . . 9
133126, 131, 132syl2anc 644 . . . . . . . 8
134 hashcl 11690 . . . . . . . 8
135 nn0p1nn 10310 . . . . . . . 8
136133, 134, 1353syl 19 . . . . . . 7
137 eluzle 10549 . . . . . . . . . . . . . . 15
138137adantl 454 . . . . . . . . . . . . . 14
139133adantr 453 . . . . . . . . . . . . . . . 16
140 nn0z 10355 . . . . . . . . . . . . . . . 16
141139, 134, 1403syl 19 . . . . . . . . . . . . . . 15
142 eluzelz 10547 . . . . . . . . . . . . . . . 16
143142adantl 454 . . . . . . . . . . . . . . 15
144 zltp1le 10376 . . . . . . . . . . . . . . 15
145141, 143, 144syl2anc 644 . . . . . . . . . . . . . 14
146138, 145mpbird 225 . . . . . . . . . . . . 13
147 nn0re 10281 . . . . . . . . . . . . . . . 16
148133, 134, 1473syl 19 . . . . . . . . . . . . . . 15
149148adantr 453 . . . . . . . . . . . . . 14
150 nnuz 10572 . . . . . . . . . . . . . . . . 17
151150uztrn2 10554 . . . . . . . . . . . . . . . 16
152136, 151sylan 459 . . . . . . . . . . . . . . 15
153152nnred 10066 . . . . . . . . . . . . . 14
154149, 153ltnled 9271 . . . . . . . . . . . . 13
155146, 154mpbid 203 . . . . . . . . . . . 12
156 fzss2 11143 . . . . . . . . . . . . . 14
157 imass2 5284 . . . . . . . . . . . . . 14
158 imass2 5284 . . . . . . . . . . . . . 14
159156, 157, 1583syl 19 . . . . . . . . . . . . 13
160 ssdomg 7202 . . . . . . . . . . . . . . 15
161139, 160syl 16 . . . . . . . . . . . . . 14
1624ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23 <