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

Theorem isercoll 12992
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 10744 . . . . . . . . . 10
31, 2eqsstri 3423 . . . . . . . . 9
4 isercoll.g . . . . . . . . . 10
54ffvelrnda 5859 . . . . . . . . 9
63, 5sseldi 3391 . . . . . . . 8
7 nnz 10532 . . . . . . . . . . . 12
87ad2antlr 709 . . . . . . . . . . 11
9 fzfid 11644 . . . . . . . . . . . . 13
10 ffun 5579 . . . . . . . . . . . . . . . 16
11 funimacnv 5508 . . . . . . . . . . . . . . . 16
124, 10, 113syl 19 . . . . . . . . . . . . . . 15
13 inss1 3606 . . . . . . . . . . . . . . 15
1412, 13syl6eqss 3443 . . . . . . . . . . . . . 14
1514ad2antrr 708 . . . . . . . . . . . . 13
16 ssfi 7494 . . . . . . . . . . . . 13
179, 15, 16syl2anc 644 . . . . . . . . . . . 12
18 hashcl 11975 . . . . . . . . . . . 12
19 nn0z 10533 . . . . . . . . . . . 12
2017, 18, 193syl 19 . . . . . . . . . . 11
21 ssid 3412 . . . . . . . . . . . . . . . . . . . 20
22 isercoll.m . . . . . . . . . . . . . . . . . . . . 21
23 isercoll.i . . . . . . . . . . . . . . . . . . . . 21
241, 22, 4, 23isercolllem1 12989 . . . . . . . . . . . . . . . . . . . 20
2521, 24mpan2 654 . . . . . . . . . . . . . . . . . . 19
26 ffn 5577 . . . . . . . . . . . . . . . . . . . 20
27 fnresdm 5538 . . . . . . . . . . . . . . . . . . . 20
28 isoeq1 6020 . . . . . . . . . . . . . . . . . . . 20
294, 26, 27, 284syl 20 . . . . . . . . . . . . . . . . . . 19
3025, 29mpbid 203 . . . . . . . . . . . . . . . . . 18
31 isof1o 6026 . . . . . . . . . . . . . . . . . 18
32 f1ocnv 5670 . . . . . . . . . . . . . . . . . 18
33 f1ofun 5660 . . . . . . . . . . . . . . . . . 18
3430, 31, 32, 334syl 20 . . . . . . . . . . . . . . . . 17
35 df-f1 5443 . . . . . . . . . . . . . . . . 17
364, 34, 35sylanbrc 647 . . . . . . . . . . . . . . . 16
3736ad2antrr 708 . . . . . . . . . . . . . . 15
38 elfznn 11334 . . . . . . . . . . . . . . . 16
3938ssriv 3397 . . . . . . . . . . . . . . 15
40 ovex 6128 . . . . . . . . . . . . . . . 16
4140f1imaen 7333 . . . . . . . . . . . . . . 15
4237, 39, 41sylancl 645 . . . . . . . . . . . . . 14
43 fzfid 11644 . . . . . . . . . . . . . . . 16
44 enfii 7491 . . . . . . . . . . . . . . . 16
4543, 42, 44syl2anc 644 . . . . . . . . . . . . . . 15
46 hashen 11967 . . . . . . . . . . . . . . 15
4745, 43, 46syl2anc 644 . . . . . . . . . . . . . 14
4842, 47mpbird 225 . . . . . . . . . . . . 13
49 nnnn0 10452 . . . . . . . . . . . . . . 15
5049ad2antlr 709 . . . . . . . . . . . . . 14
51 hashfz1 11966 . . . . . . . . . . . . . 14
5250, 51syl 16 . . . . . . . . . . . . 13
5348, 52eqtrd 2521 . . . . . . . . . . . 12
5438adantl 454 . . . . . . . . . . . . . . . . . 18
55 zssre 10517 . . . . . . . . . . . . . . . . . . . . . 22
563, 55sstri 3402 . . . . . . . . . . . . . . . . . . . . 21
574ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22
58 ffvelrn 5857 . . . . . . . . . . . . . . . . . . . . . 22
5957, 38, 58syl2an 465 . . . . . . . . . . . . . . . . . . . . 21
6056, 59sseldi 3391 . . . . . . . . . . . . . . . . . . . 20
615ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21
6256, 61sseldi 3391 . . . . . . . . . . . . . . . . . . . 20
63 eluzelz 10734 . . . . . . . . . . . . . . . . . . . . . 22
6463ad2antlr 709 . . . . . . . . . . . . . . . . . . . . 21
6564zred 10611 . . . . . . . . . . . . . . . . . . . 20
66 elfzle2 11311 . . . . . . . . . . . . . . . . . . . . . 22
6766adantl 454 . . . . . . . . . . . . . . . . . . . . 21
6830ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . 24
69 simpllr 737 . . . . . . . . . . . . . . . . . . . . . . . 24
70 isorel 6027 . . . . . . . . . . . . . . . . . . . . . . . 24
7168, 69, 54, 70syl12anc 1190 . . . . . . . . . . . . . . . . . . . . . . 23
7271notbid 287 . . . . . . . . . . . . . . . . . . . . . 22
7354nnred 10203 . . . . . . . . . . . . . . . . . . . . . . 23
7469nnred 10203 . . . . . . . . . . . . . . . . . . . . . . 23
7573, 74lenltd 9399 . . . . . . . . . . . . . . . . . . . . . 22
7660, 62lenltd 9399 . . . . . . . . . . . . . . . . . . . . . 22
7772, 75, 763bitr4d 278 . . . . . . . . . . . . . . . . . . . . 21
7867, 77mpbid 203 . . . . . . . . . . . . . . . . . . . 20
79 eluzle 10737 . . . . . . . . . . . . . . . . . . . . 21
8079ad2antlr 709 . . . . . . . . . . . . . . . . . . . 20
8160, 62, 65, 78, 80letrd 9407 . . . . . . . . . . . . . . . . . . 19
8259, 1syl6eleq 2579 . . . . . . . . . . . . . . . . . . . 20
83 elfz5 11301 . . . . . . . . . . . . . . . . . . . 20
8482, 64, 83syl2anc 644 . . . . . . . . . . . . . . . . . . 19
8581, 84mpbird 225 . . . . . . . . . . . . . . . . . 18
8657, 26syl 16 . . . . . . . . . . . . . . . . . . . 20
8786adantr 453 . . . . . . . . . . . . . . . . . . 19
88 elpreima 5839 . . . . . . . . . . . . . . . . . . 19
8987, 88syl 16 . . . . . . . . . . . . . . . . . 18
9054, 85, 89mpbir2and 890 . . . . . . . . . . . . . . . . 17
9190ex 425 . . . . . . . . . . . . . . . 16
9291ssrdv 3399 . . . . . . . . . . . . . . 15
93 imass2 5227 . . . . . . . . . . . . . . 15
9492, 93syl 16 . . . . . . . . . . . . . 14
95 ssdomg 7317 . . . . . . . . . . . . . 14
9617, 94, 95sylc 59 . . . . . . . . . . . . 13
97 hashdom 11991 . . . . . . . . . . . . . 14
9845, 17, 97syl2anc 644 . . . . . . . . . . . . 13
9996, 98mpbird 225 . . . . . . . . . . . 12
10053, 99eqbrtrrd 4340 . . . . . . . . . . 11
101 eluz2 10731 . . . . . . . . . . 11
1028, 20, 100, 101syl3anbrc 1146 . . . . . . . . . 10
103 fveq2 5708 . . . . . . . . . . . . 13
104103eleq1d 2555 . . . . . . . . . . . 12
105103oveq1d 6118 . . . . . . . . . . . . . 14
106105fveq2d 5712 . . . . . . . . . . . . 13
107106breq1d 4328 . . . . . . . . . . . 12
108104, 107anbi12d 693 . . . . . . . . . . 11
109108rspcv 3109 . . . . . . . . . 10
110102, 109syl 16 . . . . . . . . 9
111110ralrimdva 2850 . . . . . . . 8
112 fveq2 5708 . . . . . . . . . 10
113112raleqdv 2966 . . . . . . . . 9
114113rspcev 3113 . . . . . . . 8
1156, 111, 114ee12an 1382 . . . . . . 7
116115rexlimdva 2884 . . . . . 6
117 1nn 10199 . . . . . . . . 9
118 ffvelrn 5857 . . . . . . . . 9
1194, 117, 118sylancl 645 . . . . . . . 8
120119, 1syl6eleq 2579 . . . . . . 7
121 eluzelz 10734 . . . . . . 7
122 eqid 2489 . . . . . . . 8
123122rexuz3 12683 . . . . . . 7
124120, 121, 1233syl 19 . . . . . 6
125116, 124sylibrd 227 . . . . 5
126 fzfid 11644 . . . . . . . . 9
127 funimacnv 5508 . . . . . . . . . . . 12
1284, 10, 1273syl 19 . . . . . . . . . . 11
129 inss1 3606 . . . . . . . . . . 11
130128, 129syl6eqss 3443 . . . . . . . . . 10
131130adantr 453 . . . . . . . . 9
132 ssfi 7494 . . . . . . . . 9
133126, 131, 132syl2anc 644 . . . . . . . 8
134 hashcl 11975 . . . . . . . 8
135 nn0p1nn 10485 . . . . . . . 8
136133, 134, 1353syl 19 . . . . . . 7
137 eluzle 10737 . . . . . . . . . . . . . . 15
138137adantl 454 . . . . . . . . . . . . . 14
139133adantr 453 . . . . . . . . . . . . . . . 16
140 nn0z 10533 . . . . . . . . . . . . . . . 16
141139, 134, 1403syl 19 . . . . . . . . . . . . . . 15
142 eluzelz 10734 . . . . . . . . . . . . . . . 16
143142adantl 454 . . . . . . . . . . . . . . 15
144 zltp1le 10558 . . . . . . . . . . . . . . 15
145141, 143, 144syl2anc 644 . . . . . . . . . . . . . 14
146138, 145mpbird 225 . . . . . . . . . . . . 13
147 nn0re 10454 . . . . . . . . . . . . . . . 16
148133, 134, 1473syl 19 . . . . . . . . . . . . . . 15
149148adantr 453 . . . . . . . . . . . . . 14
150 eluznn 10789 . . . . . . . . . . . . . . . 16
151136, 150sylan 459 . . . . . . . . . . . . . . 15
152151nnred 10203 . . . . . . . . . . . . . 14
153149, 152ltnled 9400 . . . . . . . . . . . . 13
154146, 153mpbid 203 . . . . . . . . . . . 12
155 fzss2 11354 . . . . . . . . . . . . . 14
156 imass2 5227 . . . . . . . . . . . . . 14
157 imass2 5227 . . . . . . . . . . . . . 14
158155, 156, 1573syl 19 . . . . . . . . . . . . 13
159 ssdomg 7317 . . . . . . . . . . . . . . 15
160139, 159syl 16 . . . . . . . . . . . . . 14
1614ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23