Metamath Proof Explorer


Theorem sge0f1o

Description: Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0f1o.1 k φ
sge0f1o.2 n φ
sge0f1o.3 k = G B = D
sge0f1o.4 φ C V
sge0f1o.5 φ F : C 1-1 onto A
sge0f1o.6 φ n C F n = G
sge0f1o.7 φ k A B 0 +∞
Assertion sge0f1o φ sum^ k A B = sum^ n C D

Proof

Step Hyp Ref Expression
1 sge0f1o.1 k φ
2 sge0f1o.2 n φ
3 sge0f1o.3 k = G B = D
4 sge0f1o.4 φ C V
5 sge0f1o.5 φ F : C 1-1 onto A
6 sge0f1o.6 φ n C F n = G
7 sge0f1o.7 φ k A B 0 +∞
8 f1ofo F : C 1-1 onto A F : C onto A
9 5 8 syl φ F : C onto A
10 focdmex C V F : C onto A A V
11 4 9 10 sylc φ A V
12 11 adantr φ +∞ ran n C D A V
13 1 7 fmptd2f φ k A B : A 0 +∞
14 13 adantr φ +∞ ran n C D k A B : A 0 +∞
15 nfv n +∞ ran k A B
16 simp3 φ n C +∞ = D +∞ = D
17 f1of F : C 1-1 onto A F : C A
18 5 17 syl φ F : C A
19 18 ffvelcdmda φ n C F n A
20 nfv k F n = G
21 nfcsb1v _ k F n / k B
22 21 nfeq1 k F n / k B = D
23 20 22 nfim k F n = G F n / k B = D
24 eqeq1 k = F n k = G F n = G
25 csbeq1a k = F n B = F n / k B
26 25 eqeq1d k = F n B = D F n / k B = D
27 24 26 imbi12d k = F n k = G B = D F n = G F n / k B = D
28 23 27 3 vtoclg1f F n A F n = G F n / k B = D
29 19 6 28 sylc φ n C F n / k B = D
30 29 eqcomd φ n C D = F n / k B
31 30 3adant3 φ n C +∞ = D D = F n / k B
32 16 31 eqtrd φ n C +∞ = D +∞ = F n / k B
33 simpl φ n C φ
34 33 19 jca φ n C φ F n A
35 nfv k F n A
36 1 35 nfan k φ F n A
37 21 nfel1 k F n / k B 0 +∞
38 36 37 nfim k φ F n A F n / k B 0 +∞
39 eleq1 k = F n k A F n A
40 39 anbi2d k = F n φ k A φ F n A
41 25 eleq1d k = F n B 0 +∞ F n / k B 0 +∞
42 40 41 imbi12d k = F n φ k A B 0 +∞ φ F n A F n / k B 0 +∞
43 38 42 7 vtoclg1f F n A φ F n A F n / k B 0 +∞
44 19 34 43 sylc φ n C F n / k B 0 +∞
45 eqid k A B = k A B
46 21 45 25 elrnmpt1sf F n A F n / k B 0 +∞ F n / k B ran k A B
47 19 44 46 syl2anc φ n C F n / k B ran k A B
48 47 3adant3 φ n C +∞ = D F n / k B ran k A B
49 32 48 eqeltrd φ n C +∞ = D +∞ ran k A B
50 49 3exp φ n C +∞ = D +∞ ran k A B
51 2 15 50 rexlimd φ n C +∞ = D +∞ ran k A B
52 pnfex +∞ V
53 eqid n C D = n C D
54 53 elrnmpt +∞ V +∞ ran n C D n C +∞ = D
55 52 54 ax-mp +∞ ran n C D n C +∞ = D
56 55 biimpi +∞ ran n C D n C +∞ = D
57 51 56 impel φ +∞ ran n C D +∞ ran k A B
58 12 14 57 sge0pnfval φ +∞ ran n C D sum^ k A B = +∞
59 4 adantr φ +∞ ran n C D C V
60 30 44 eqeltrd φ n C D 0 +∞
61 2 60 fmptd2f φ n C D : C 0 +∞
62 61 adantr φ +∞ ran n C D n C D : C 0 +∞
63 simpr φ +∞ ran n C D +∞ ran n C D
64 59 62 63 sge0pnfval φ +∞ ran n C D sum^ n C D = +∞
65 58 64 eqtr4d φ +∞ ran n C D sum^ k A B = sum^ n C D
66 sumex k y B V
67 66 a1i φ ¬ +∞ ran n C D y 𝒫 A Fin k y B V
68 cnvimass F -1 y dom F
69 68 18 fssdm φ F -1 y C
70 4 69 sselpwd φ F -1 y 𝒫 C
71 70 adantr φ y 𝒫 A Fin F -1 y 𝒫 C
72 f1ocnv F : C 1-1 onto A F -1 : A 1-1 onto C
73 5 72 syl φ F -1 : A 1-1 onto C
74 f1ofun F -1 : A 1-1 onto C Fun F -1
75 73 74 syl φ Fun F -1
76 elinel2 y 𝒫 A Fin y Fin
77 imafi Fun F -1 y Fin F -1 y Fin
78 75 76 77 syl2an φ y 𝒫 A Fin F -1 y Fin
79 71 78 elind φ y 𝒫 A Fin F -1 y 𝒫 C Fin
80 79 adantlr φ ¬ +∞ ran n C D y 𝒫 A Fin F -1 y 𝒫 C Fin
81 nfv k ¬ +∞ ran n C D
82 1 81 nfan k φ ¬ +∞ ran n C D
83 nfv k y 𝒫 A Fin
84 82 83 nfan k φ ¬ +∞ ran n C D y 𝒫 A Fin
85 nfmpt1 _ n n C D
86 85 nfrn _ n ran n C D
87 86 nfel2 n +∞ ran n C D
88 87 nfn n ¬ +∞ ran n C D
89 2 88 nfan n φ ¬ +∞ ran n C D
90 nfv n y 𝒫 A Fin
91 89 90 nfan n φ ¬ +∞ ran n C D y 𝒫 A Fin
92 78 adantlr φ ¬ +∞ ran n C D y 𝒫 A Fin F -1 y Fin
93 f1of1 F : C 1-1 onto A F : C 1-1 A
94 5 93 syl φ F : C 1-1 A
95 94 adantr φ y 𝒫 A Fin F : C 1-1 A
96 69 adantr φ y 𝒫 A Fin F -1 y C
97 f1ores F : C 1-1 A F -1 y C F F -1 y : F -1 y 1-1 onto F F -1 y
98 95 96 97 syl2anc φ y 𝒫 A Fin F F -1 y : F -1 y 1-1 onto F F -1 y
99 elpwinss y 𝒫 A Fin y A
100 foimacnv F : C onto A y A F F -1 y = y
101 9 99 100 syl2an φ y 𝒫 A Fin F F -1 y = y
102 101 f1oeq3d φ y 𝒫 A Fin F F -1 y : F -1 y 1-1 onto F F -1 y F F -1 y : F -1 y 1-1 onto y
103 98 102 mpbid φ y 𝒫 A Fin F F -1 y : F -1 y 1-1 onto y
104 103 adantlr φ ¬ +∞ ran n C D y 𝒫 A Fin F F -1 y : F -1 y 1-1 onto y
105 18 4 fexd φ F V
106 cnvexg F V F -1 V
107 105 106 syl φ F -1 V
108 107 imaexd φ F -1 y V
109 108 ad2antrr φ y 𝒫 A Fin n F -1 y F -1 y V
110 simpll φ y 𝒫 A Fin n F -1 y φ
111 79 adantr φ y 𝒫 A Fin n F -1 y F -1 y 𝒫 C Fin
112 simpr φ y 𝒫 A Fin n F -1 y n F -1 y
113 110 111 112 jca31 φ y 𝒫 A Fin n F -1 y φ F -1 y 𝒫 C Fin n F -1 y
114 eleq1 x = F -1 y x 𝒫 C Fin F -1 y 𝒫 C Fin
115 114 anbi2d x = F -1 y φ x 𝒫 C Fin φ F -1 y 𝒫 C Fin
116 eleq2w2 x = F -1 y n x n F -1 y
117 115 116 anbi12d x = F -1 y φ x 𝒫 C Fin n x φ F -1 y 𝒫 C Fin n F -1 y
118 reseq2 x = F -1 y F x = F F -1 y
119 118 fveq1d x = F -1 y F x n = F F -1 y n
120 119 eqeq1d x = F -1 y F x n = G F F -1 y n = G
121 117 120 imbi12d x = F -1 y φ x 𝒫 C Fin n x F x n = G φ F -1 y 𝒫 C Fin n F -1 y F F -1 y n = G
122 fvres n x F x n = F n
123 122 adantl φ x 𝒫 C Fin n x F x n = F n
124 simpll φ x 𝒫 C Fin n x φ
125 elpwinss x 𝒫 C Fin x C
126 125 adantl φ x 𝒫 C Fin x C
127 126 sselda φ x 𝒫 C Fin n x n C
128 124 127 6 syl2anc φ x 𝒫 C Fin n x F n = G
129 123 128 eqtrd φ x 𝒫 C Fin n x F x n = G
130 121 129 vtoclg F -1 y V φ F -1 y 𝒫 C Fin n F -1 y F F -1 y n = G
131 109 113 130 sylc φ y 𝒫 A Fin n F -1 y F F -1 y n = G
132 131 adantllr φ ¬ +∞ ran n C D y 𝒫 A Fin n F -1 y F F -1 y n = G
133 108 ad3antrrr φ ¬ +∞ ran n C D y 𝒫 A Fin k y F -1 y V
134 simpll φ ¬ +∞ ran n C D y 𝒫 A Fin k y φ ¬ +∞ ran n C D
135 70 ad3antrrr φ ¬ +∞ ran n C D y 𝒫 A Fin k y F -1 y 𝒫 C
136 92 adantr φ ¬ +∞ ran n C D y 𝒫 A Fin k y F -1 y Fin
137 135 136 elind φ ¬ +∞ ran n C D y 𝒫 A Fin k y F -1 y 𝒫 C Fin
138 simpr φ y 𝒫 A Fin k y k y
139 101 eqcomd φ y 𝒫 A Fin y = F F -1 y
140 139 adantr φ y 𝒫 A Fin k y y = F F -1 y
141 138 140 eleqtrd φ y 𝒫 A Fin k y k F F -1 y
142 141 adantllr φ ¬ +∞ ran n C D y 𝒫 A Fin k y k F F -1 y
143 134 137 142 jca31 φ ¬ +∞ ran n C D y 𝒫 A Fin k y φ ¬ +∞ ran n C D F -1 y 𝒫 C Fin k F F -1 y
144 114 anbi2d x = F -1 y φ ¬ +∞ ran n C D x 𝒫 C Fin φ ¬ +∞ ran n C D F -1 y 𝒫 C Fin
145 imaeq2 x = F -1 y F x = F F -1 y
146 145 eleq2d x = F -1 y k F x k F F -1 y
147 144 146 anbi12d x = F -1 y φ ¬ +∞ ran n C D x 𝒫 C Fin k F x φ ¬ +∞ ran n C D F -1 y 𝒫 C Fin k F F -1 y
148 147 imbi1d x = F -1 y φ ¬ +∞ ran n C D x 𝒫 C Fin k F x B φ ¬ +∞ ran n C D F -1 y 𝒫 C Fin k F F -1 y B
149 rge0ssre 0 +∞
150 ax-resscn
151 149 150 sstri 0 +∞
152 simplll φ ¬ +∞ ran n C D x 𝒫 C Fin k F x φ
153 simpllr φ ¬ +∞ ran n C D x 𝒫 C Fin k F x ¬ +∞ ran n C D
154 18 fimassd φ F x A
155 154 ad2antrr φ x 𝒫 C Fin k F x F x A
156 simpr φ x 𝒫 C Fin k F x k F x
157 155 156 sseldd φ x 𝒫 C Fin k F x k A
158 157 adantllr φ ¬ +∞ ran n C D x 𝒫 C Fin k F x k A
159 foelcdmi F : C onto A k A n C F n = k
160 9 159 sylan φ k A n C F n = k
161 160 adantlr φ ¬ +∞ ran n C D k A n C F n = k
162 nfv n k A
163 89 162 nfan n φ ¬ +∞ ran n C D k A
164 nfv n B 0 +∞
165 csbid k / k B = B
166 165 eqcomi B = k / k B
167 166 a1i φ n C F n = k B = k / k B
168 id F n = k F n = k
169 168 eqcomd F n = k k = F n
170 169 csbeq1d F n = k k / k B = F n / k B
171 170 3ad2ant3 φ n C F n = k k / k B = F n / k B
172 29 3adant3 φ n C F n = k F n / k B = D
173 167 171 172 3eqtrd φ n C F n = k B = D
174 173 3adant1r φ ¬ +∞ ran n C D n C F n = k B = D
175 0xr 0 *
176 175 a1i φ n C ¬ D 0 +∞ 0 *
177 pnfxr +∞ *
178 177 a1i φ n C ¬ D 0 +∞ +∞ *
179 60 adantr φ n C ¬ D 0 +∞ D 0 +∞
180 simpr φ n C ¬ D 0 +∞ ¬ D 0 +∞
181 176 178 179 180 eliccnelico φ n C ¬ D 0 +∞ D = +∞
182 181 eqcomd φ n C ¬ D 0 +∞ +∞ = D
183 simpr φ n C n C
184 53 183 60 elrnmpt1d φ n C D ran n C D
185 184 adantr φ n C ¬ D 0 +∞ D ran n C D
186 182 185 eqeltrd φ n C ¬ D 0 +∞ +∞ ran n C D
187 186 adantllr φ ¬ +∞ ran n C D n C ¬ D 0 +∞ +∞ ran n C D
188 simpllr φ ¬ +∞ ran n C D n C ¬ D 0 +∞ ¬ +∞ ran n C D
189 187 188 condan φ ¬ +∞ ran n C D n C D 0 +∞
190 189 3adant3 φ ¬ +∞ ran n C D n C F n = k D 0 +∞
191 174 190 eqeltrd φ ¬ +∞ ran n C D n C F n = k B 0 +∞
192 191 3exp φ ¬ +∞ ran n C D n C F n = k B 0 +∞
193 192 adantr φ ¬ +∞ ran n C D k A n C F n = k B 0 +∞
194 163 164 193 rexlimd φ ¬ +∞ ran n C D k A n C F n = k B 0 +∞
195 161 194 mpd φ ¬ +∞ ran n C D k A B 0 +∞
196 152 153 158 195 syl21anc φ ¬ +∞ ran n C D x 𝒫 C Fin k F x B 0 +∞
197 151 196 sselid φ ¬ +∞ ran n C D x 𝒫 C Fin k F x B
198 148 197 vtoclg F -1 y V φ ¬ +∞ ran n C D F -1 y 𝒫 C Fin k F F -1 y B
199 133 143 198 sylc φ ¬ +∞ ran n C D y 𝒫 A Fin k y B
200 84 91 3 92 104 132 199 fsumf1of φ ¬ +∞ ran n C D y 𝒫 A Fin k y B = n F -1 y D
201 sumeq1 x = F -1 y n x D = n F -1 y D
202 201 rspceeqv F -1 y 𝒫 C Fin k y B = n F -1 y D x 𝒫 C Fin k y B = n x D
203 80 200 202 syl2anc φ ¬ +∞ ran n C D y 𝒫 A Fin x 𝒫 C Fin k y B = n x D
204 67 203 rnmptssrn φ ¬ +∞ ran n C D ran y 𝒫 A Fin k y B ran x 𝒫 C Fin n x D
205 sumex n x D V
206 205 a1i φ ¬ +∞ ran n C D x 𝒫 C Fin n x D V
207 11 154 sselpwd φ F x 𝒫 A
208 207 adantr φ x 𝒫 C Fin F x 𝒫 A
209 18 ffund φ Fun F
210 elinel2 x 𝒫 C Fin x Fin
211 imafi Fun F x Fin F x Fin
212 209 210 211 syl2an φ x 𝒫 C Fin F x Fin
213 208 212 elind φ x 𝒫 C Fin F x 𝒫 A Fin
214 213 adantlr φ ¬ +∞ ran n C D x 𝒫 C Fin F x 𝒫 A Fin
215 nfv k x 𝒫 C Fin
216 82 215 nfan k φ ¬ +∞ ran n C D x 𝒫 C Fin
217 nfv n x 𝒫 C Fin
218 89 217 nfan n φ ¬ +∞ ran n C D x 𝒫 C Fin
219 210 adantl φ ¬ +∞ ran n C D x 𝒫 C Fin x Fin
220 f1ores F : C 1-1 A x C F x : x 1-1 onto F x
221 94 125 220 syl2an φ x 𝒫 C Fin F x : x 1-1 onto F x
222 221 adantlr φ ¬ +∞ ran n C D x 𝒫 C Fin F x : x 1-1 onto F x
223 129 adantllr φ ¬ +∞ ran n C D x 𝒫 C Fin n x F x n = G
224 216 218 3 219 222 223 197 fsumf1of φ ¬ +∞ ran n C D x 𝒫 C Fin k F x B = n x D
225 224 eqcomd φ ¬ +∞ ran n C D x 𝒫 C Fin n x D = k F x B
226 sumeq1 y = F x k y B = k F x B
227 226 rspceeqv F x 𝒫 A Fin n x D = k F x B y 𝒫 A Fin n x D = k y B
228 214 225 227 syl2anc φ ¬ +∞ ran n C D x 𝒫 C Fin y 𝒫 A Fin n x D = k y B
229 206 228 rnmptssrn φ ¬ +∞ ran n C D ran x 𝒫 C Fin n x D ran y 𝒫 A Fin k y B
230 204 229 eqssd φ ¬ +∞ ran n C D ran y 𝒫 A Fin k y B = ran x 𝒫 C Fin n x D
231 230 supeq1d φ ¬ +∞ ran n C D sup ran y 𝒫 A Fin k y B * < = sup ran x 𝒫 C Fin n x D * <
232 11 adantr φ ¬ +∞ ran n C D A V
233 82 232 195 sge0revalmpt φ ¬ +∞ ran n C D sum^ k A B = sup ran y 𝒫 A Fin k y B * <
234 4 adantr φ ¬ +∞ ran n C D C V
235 89 234 189 sge0revalmpt φ ¬ +∞ ran n C D sum^ n C D = sup ran x 𝒫 C Fin n x D * <
236 231 233 235 3eqtr4d φ ¬ +∞ ran n C D sum^ k A B = sum^ n C D
237 65 236 pm2.61dan φ sum^ k A B = sum^ n C D