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

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.
StepHypRef Expression
1 isercoll.z . . . . . . . . . 10
2 uzssz 11129 . . . . . . . . . 10
31, 2eqsstri 3533 . . . . . . . . 9
4 isercoll.g . . . . . . . . . 10
54ffvelrnda 6031 . . . . . . . . 9
63, 5sseldi 3501 . . . . . . . 8
7 nnz 10911 . . . . . . . . . . . 12
87ad2antlr 726 . . . . . . . . . . 11
9 fzfid 12083 . . . . . . . . . . . . 13
10 ffun 5738 . . . . . . . . . . . . . . . 16
11 funimacnv 5665 . . . . . . . . . . . . . . . 16
124, 10, 113syl 20 . . . . . . . . . . . . . . 15
13 inss1 3717 . . . . . . . . . . . . . . 15
1412, 13syl6eqss 3553 . . . . . . . . . . . . . 14
1514ad2antrr 725 . . . . . . . . . . . . 13
16 ssfi 7760 . . . . . . . . . . . . 13
179, 15, 16syl2anc 661 . . . . . . . . . . . 12
18 hashcl 12428 . . . . . . . . . . . 12
19 nn0z 10912 . . . . . . . . . . . 12
2017, 18, 193syl 20 . . . . . . . . . . 11
21 ssid 3522 . . . . . . . . . . . . . . . . . . . 20
22 isercoll.m . . . . . . . . . . . . . . . . . . . . 21
23 isercoll.i . . . . . . . . . . . . . . . . . . . . 21
241, 22, 4, 23isercolllem1 13487 . . . . . . . . . . . . . . . . . . . 20
2521, 24mpan2 671 . . . . . . . . . . . . . . . . . . 19
26 ffn 5736 . . . . . . . . . . . . . . . . . . . 20
27 fnresdm 5695 . . . . . . . . . . . . . . . . . . . 20
28 isoeq1 6215 . . . . . . . . . . . . . . . . . . . 20
294, 26, 27, 284syl 21 . . . . . . . . . . . . . . . . . . 19
3025, 29mpbid 210 . . . . . . . . . . . . . . . . . 18
31 isof1o 6221 . . . . . . . . . . . . . . . . . 18
32 f1ocnv 5833 . . . . . . . . . . . . . . . . . 18
33 f1ofun 5823 . . . . . . . . . . . . . . . . . 18
3430, 31, 32, 334syl 21 . . . . . . . . . . . . . . . . 17
35 df-f1 5598 . . . . . . . . . . . . . . . . 17
364, 34, 35sylanbrc 664 . . . . . . . . . . . . . . . 16
3736ad2antrr 725 . . . . . . . . . . . . . . 15
38 elfznn 11743 . . . . . . . . . . . . . . . 16
3938ssriv 3507 . . . . . . . . . . . . . . 15
40 ovex 6324 . . . . . . . . . . . . . . . 16
4140f1imaen 7597 . . . . . . . . . . . . . . 15
4237, 39, 41sylancl 662 . . . . . . . . . . . . . 14
43 fzfid 12083 . . . . . . . . . . . . . . . 16
44 enfii 7757 . . . . . . . . . . . . . . . 16
4543, 42, 44syl2anc 661 . . . . . . . . . . . . . . 15
46 hashen 12420 . . . . . . . . . . . . . . 15
4745, 43, 46syl2anc 661 . . . . . . . . . . . . . 14
4842, 47mpbird 232 . . . . . . . . . . . . 13
49 nnnn0 10827 . . . . . . . . . . . . . . 15
5049ad2antlr 726 . . . . . . . . . . . . . 14
51 hashfz1 12419 . . . . . . . . . . . . . 14
5250, 51syl 16 . . . . . . . . . . . . 13
5348, 52eqtrd 2498 . . . . . . . . . . . 12
5438adantl 466 . . . . . . . . . . . . . . . . . 18
55 zssre 10896 . . . . . . . . . . . . . . . . . . . . . 22
563, 55sstri 3512 . . . . . . . . . . . . . . . . . . . . 21
574ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22
58 ffvelrn 6029 . . . . . . . . . . . . . . . . . . . . . 22
5957, 38, 58syl2an 477 . . . . . . . . . . . . . . . . . . . . 21
6056, 59sseldi 3501 . . . . . . . . . . . . . . . . . . . 20
615ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
6256, 61sseldi 3501 . . . . . . . . . . . . . . . . . . . 20
63 eluzelz 11119 . . . . . . . . . . . . . . . . . . . . . 22
6463ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21
6564zred 10994 . . . . . . . . . . . . . . . . . . . 20
66 elfzle2 11719 . . . . . . . . . . . . . . . . . . . . . 22
6766adantl 466 . . . . . . . . . . . . . . . . . . . . 21
6830ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . 24
69 simpllr 760 . . . . . . . . . . . . . . . . . . . . . . . 24
70 isorel 6222 . . . . . . . . . . . . . . . . . . . . . . . 24
7168, 69, 54, 70syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . . 23
7271notbid 294 . . . . . . . . . . . . . . . . . . . . . 22
7354nnred 10576 . . . . . . . . . . . . . . . . . . . . . . 23
7469nnred 10576 . . . . . . . . . . . . . . . . . . . . . . 23
7573, 74lenltd 9752 . . . . . . . . . . . . . . . . . . . . . 22
7660, 62lenltd 9752 . . . . . . . . . . . . . . . . . . . . . 22
7772, 75, 763bitr4d 285 . . . . . . . . . . . . . . . . . . . . 21
7867, 77mpbid 210 . . . . . . . . . . . . . . . . . . . 20
79 eluzle 11122 . . . . . . . . . . . . . . . . . . . . 21
8079ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20
8160, 62, 65, 78, 80letrd 9760 . . . . . . . . . . . . . . . . . . 19
8259, 1syl6eleq 2555 . . . . . . . . . . . . . . . . . . . 20
83 elfz5 11709 . . . . . . . . . . . . . . . . . . . 20
8482, 64, 83syl2anc 661 . . . . . . . . . . . . . . . . . . 19
8581, 84mpbird 232 . . . . . . . . . . . . . . . . . 18
8657, 26syl 16 . . . . . . . . . . . . . . . . . . . 20
8786adantr 465 . . . . . . . . . . . . . . . . . . 19
88 elpreima 6007 . . . . . . . . . . . . . . . . . . 19
8987, 88syl 16 . . . . . . . . . . . . . . . . . 18
9054, 85, 89mpbir2and 922 . . . . . . . . . . . . . . . . 17
9190ex 434 . . . . . . . . . . . . . . . 16
9291ssrdv 3509 . . . . . . . . . . . . . . 15
93 imass2 5377 . . . . . . . . . . . . . . 15
9492, 93syl 16 . . . . . . . . . . . . . 14
95 ssdomg 7581 . . . . . . . . . . . . . 14
9617, 94, 95sylc 60 . . . . . . . . . . . . 13
97 hashdom 12447 . . . . . . . . . . . . . 14
9845, 17, 97syl2anc 661 . . . . . . . . . . . . 13
9996, 98mpbird 232 . . . . . . . . . . . 12
10053, 99eqbrtrrd 4474 . . . . . . . . . . 11
101 eluz2 11116 . . . . . . . . . . 11
1028, 20, 100, 101syl3anbrc 1180 . . . . . . . . . 10
103 fveq2 5871 . . . . . . . . . . . . 13
104103eleq1d 2526 . . . . . . . . . . . 12
105103oveq1d 6311 . . . . . . . . . . . . . 14
106105fveq2d 5875 . . . . . . . . . . . . 13
107106breq1d 4462 . . . . . . . . . . . 12
108104, 107anbi12d 710 . . . . . . . . . . 11
109108rspcv 3206 . . . . . . . . . 10
110102, 109syl 16 . . . . . . . . 9
111110ralrimdva 2875 . . . . . . . 8
112 fveq2 5871 . . . . . . . . . 10
113112raleqdv 3060 . . . . . . . . 9
114113rspcev 3210 . . . . . . . 8
1156, 111, 114syl6an 545 . . . . . . 7
116115rexlimdva 2949 . . . . . 6
117 1nn 10572 . . . . . . . . 9
118 ffvelrn 6029 . . . . . . . . 9
1194, 117, 118sylancl 662 . . . . . . . 8
120119, 1syl6eleq 2555 . . . . . . 7
121 eluzelz 11119 . . . . . . 7
122 eqid 2457 . . . . . . . 8
123122rexuz3 13181 . . . . . . 7
124120, 121, 1233syl 20 . . . . . 6
125116, 124sylibrd 234 . . . . 5
126 fzfid 12083 . . . . . . . . 9
127 funimacnv 5665 . . . . . . . . . . . 12
1284, 10, 1273syl 20 . . . . . . . . . . 11
129 inss1 3717 . . . . . . . . . . 11
130128, 129syl6eqss 3553 . . . . . . . . . 10
131130adantr 465 . . . . . . . . 9
132 ssfi 7760 . . . . . . . . 9
133126, 131, 132syl2anc 661 . . . . . . . 8
134 hashcl 12428 . . . . . . . 8
135 nn0p1nn 10860 . . . . . . . 8
136133, 134, 1353syl 20 . . . . . . 7
137 eluzle 11122 . . . . . . . . . . . . . . 15
138137adantl 466 . . . . . . . . . . . . . 14
139133adantr 465 . . . . . . . . . . . . . . . 16
140 nn0z 10912 . . . . . . . . . . . . . . . 16
141139, 134, 1403syl 20 . . . . . . . . . . . . . . 15
142 eluzelz 11119 . . . . . . . . . . . . . . . 16
143142adantl 466 . . . . . . . . . . . . . . 15
144 zltp1le 10938 . . . . . . . . . . . . . . 15
145141, 143, 144syl2anc 661 . . . . . . . . . . . . . 14
146138, 145mpbird 232 . . . . . . . . . . . . 13
147 nn0re 10829 . . . . . . . . . . . . . . . 16
148133, 134, 1473syl 20 . . . . . . . . . . . . . . 15
149148adantr 465 . . . . . . . . . . . . . 14
150 eluznn 11181 . . . . . . . . . . . . . . . 16
151136, 150sylan 471 . . . . . . . . . . . . . . 15
152151nnred 10576 . . . . . . . . . . . . . 14
153149, 152ltnled 9753 . . . . . . . . . . . . 13
154146, 153mpbid 210 . . . . . . . . . . . 12
155 fzss2 11752 . . . . . . . . . . . . . 14
156 imass2 5377 . . . . . . . . . . . . . 14
157 imass2 5377 . . . . . . . . . . . . . 14
158155, 156, 1573syl 20 . . . . . . . . . . . . 13
159 ssdomg 7581 . . . . . . . . . . . . . . 15
160139, 159syl 16 . . . . . . . . . . . . . 14
1614ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23