Metamath Proof Explorer


Theorem radcnvrat

Description: Let L be the limit, if one exists, of the ratio ( abs( ( A( k + 1 ) ) / ( Ak ) ) ) (as in the ratio test cvgdvgrat ) as k increases. Then the radius of convergence of power series sum_ n e. NN0 ( ( An ) x. ( x ^ n ) ) is ( 1 / L ) if L is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020)

Ref Expression
Hypotheses radcnvrat.g G = x n 0 A n x n
radcnvrat.a φ A : 0
radcnvrat.r R = sup r | seq 0 + G r dom * <
radcnvrat.rat D = k 0 A k + 1 A k
radcnvrat.z Z = M
radcnvrat.m φ M 0
radcnvrat.n0 φ k Z A k 0
radcnvrat.l φ D L
radcnvrat.ln0 φ L 0
Assertion radcnvrat φ R = 1 L

Proof

Step Hyp Ref Expression
1 radcnvrat.g G = x n 0 A n x n
2 radcnvrat.a φ A : 0
3 radcnvrat.r R = sup r | seq 0 + G r dom * <
4 radcnvrat.rat D = k 0 A k + 1 A k
5 radcnvrat.z Z = M
6 radcnvrat.m φ M 0
7 radcnvrat.n0 φ k Z A k 0
8 radcnvrat.l φ D L
9 radcnvrat.ln0 φ L 0
10 xrltso < Or *
11 10 a1i φ < Or *
12 6 nn0zd φ M
13 5 reseq2i D Z = D M
14 nn0ex 0 V
15 14 mptex k 0 A k + 1 A k V
16 4 15 eqeltri D V
17 climres M D V D M L D L
18 12 16 17 sylancl φ D M L D L
19 8 18 mpbird φ D M L
20 13 19 eqbrtrid φ D Z L
21 4 reseq1i D Z = k 0 A k + 1 A k Z
22 eluznn0 M 0 k M k 0
23 6 22 sylan φ k M k 0
24 23 ex φ k M k 0
25 24 ssrdv φ M 0
26 5 25 eqsstrid φ Z 0
27 26 resmptd φ k 0 A k + 1 A k Z = k Z A k + 1 A k
28 21 27 syl5eq φ D Z = k Z A k + 1 A k
29 fvexd φ k Z A k + 1 A k V
30 28 29 fvmpt2d φ k Z D Z k = A k + 1 A k
31 5 peano2uzs k Z k + 1 Z
32 26 sselda φ k + 1 Z k + 1 0
33 2 ffvelrnda φ k + 1 0 A k + 1
34 32 33 syldan φ k + 1 Z A k + 1
35 31 34 sylan2 φ k Z A k + 1
36 26 sselda φ k Z k 0
37 2 ffvelrnda φ k 0 A k
38 36 37 syldan φ k Z A k
39 35 38 7 divcld φ k Z A k + 1 A k
40 39 abscld φ k Z A k + 1 A k
41 30 40 eqeltrd φ k Z D Z k
42 5 12 20 41 climrecl φ L
43 42 9 rereccld φ 1 L
44 43 rexrd φ 1 L *
45 simpr φ x r | seq 0 + G r dom x r | seq 0 + G r dom
46 elrabi x r | seq 0 + G r dom x
47 43 adantr φ x 1 L
48 recn x x
49 48 abscld x x
50 49 adantl φ x x
51 47 50 ltlend φ x 1 L < x 1 L x x 1 L
52 51 simplbda φ x 1 L < x x 1 L
53 51 adantr φ x x 1 L 1 L < x 1 L x x 1 L
54 simpr φ x x 1 L x 1 L
55 54 biantrud φ x x 1 L 1 L x 1 L x x 1 L
56 47 50 lenltd φ x 1 L x ¬ x < 1 L
57 56 adantr φ x x 1 L 1 L x ¬ x < 1 L
58 53 55 57 3bitr2d φ x x 1 L 1 L < x ¬ x < 1 L
59 1cnd φ x 1
60 50 recnd φ x x
61 42 recnd φ L
62 61 adantr φ x L
63 9 adantr φ x L 0
64 59 60 62 63 divmul3d φ x 1 L = x 1 = x L
65 eqcom 1 L = x x = 1 L
66 eqcom 1 = x L x L = 1
67 64 65 66 3bitr3g φ x x = 1 L x L = 1
68 67 necon3bid φ x x 1 L x L 1
69 68 biimpa φ x x 1 L x L 1
70 1red φ x 1
71 fvres k Z D Z k = D k
72 71 adantl φ k Z D Z k = D k
73 72 41 eqeltrrd φ k Z D k
74 39 absge0d φ k Z 0 A k + 1 A k
75 74 30 breqtrrd φ k Z 0 D Z k
76 75 72 breqtrd φ k Z 0 D k
77 5 12 8 73 76 climge0 φ 0 L
78 42 77 9 ne0gt0d φ 0 < L
79 42 78 elrpd φ L +
80 79 adantr φ x L +
81 50 70 80 ltmuldivd φ x x L < 1 x < 1 L
82 81 adantr φ x x L 1 x L < 1 x < 1 L
83 elun x 0 0 x 0 x 0
84 inundif 0 0 =
85 84 eleq2i x 0 0 x
86 83 85 bitr3i x 0 x 0 x
87 elin x 0 x x 0
88 87 simprbi x 0 x 0
89 elsni x 0 x = 0
90 88 89 syl x 0 x = 0
91 fveq2 x = 0 x = 0
92 abs0 0 = 0
93 91 92 eqtrdi x = 0 x = 0
94 93 oveq1d x = 0 x L = 0 L
95 61 mul02d φ 0 L = 0
96 94 95 sylan9eqr φ x = 0 x L = 0
97 0lt1 0 < 1
98 96 97 eqbrtrdi φ x = 0 x L < 1
99 1 2 radcnv0 φ 0 r | seq 0 + G r dom
100 eleq1 x = 0 x r | seq 0 + G r dom 0 r | seq 0 + G r dom
101 99 100 syl5ibrcom φ x = 0 x r | seq 0 + G r dom
102 101 imp φ x = 0 x r | seq 0 + G r dom
103 98 102 2thd φ x = 0 x L < 1 x r | seq 0 + G r dom
104 90 103 sylan2 φ x 0 x L < 1 x r | seq 0 + G r dom
105 104 adantlr φ x L 1 x 0 x L < 1 x r | seq 0 + G r dom
106 ax-resscn
107 ssdif 0 0
108 106 107 ax-mp 0 0
109 108 sseli x 0 x 0
110 nn0uz 0 = 0
111 6 ad2antrr φ x 0 x L 1 M 0
112 fvexd φ x 0 x L 1 G x V
113 eldifi x 0 x
114 1 a1i φ G = x n 0 A n x n
115 14 mptex n 0 A n x n V
116 115 a1i φ x n 0 A n x n V
117 114 116 fvmpt2d φ x G x = n 0 A n x n
118 117 adantr φ x k 0 G x = n 0 A n x n
119 fveq2 n = k A n = A k
120 oveq2 n = k x n = x k
121 119 120 oveq12d n = k A n x n = A k x k
122 121 adantl φ x k 0 n = k A n x n = A k x k
123 simpr φ x k 0 k 0
124 ovexd φ x k 0 A k x k V
125 118 122 123 124 fvmptd φ x k 0 G x k = A k x k
126 37 adantlr φ x k 0 A k
127 simplr φ x k 0 x
128 127 123 expcld φ x k 0 x k
129 126 128 mulcld φ x k 0 A k x k
130 125 129 eqeltrd φ x k 0 G x k
131 113 130 sylanl2 φ x 0 k 0 G x k
132 131 adantlr φ x 0 x L 1 k 0 G x k
133 36 adantlr φ x k Z k 0
134 133 125 syldan φ x k Z G x k = A k x k
135 113 134 sylanl2 φ x 0 k Z G x k = A k x k
136 38 adantlr φ x 0 k Z A k
137 113 adantl φ x 0 x
138 137 adantr φ x 0 k Z x
139 36 adantlr φ x 0 k Z k 0
140 138 139 expcld φ x 0 k Z x k
141 7 adantlr φ x 0 k Z A k 0
142 eldifsni x 0 x 0
143 142 ad2antlr φ x 0 k Z x 0
144 139 nn0zd φ x 0 k Z k
145 138 143 144 expne0d φ x 0 k Z x k 0
146 136 140 141 145 mulne0d φ x 0 k Z A k x k 0
147 135 146 eqnetrd φ x 0 k Z G x k 0
148 147 adantlr φ x 0 x L 1 k Z G x k 0
149 fvoveq1 n = k G x n + 1 = G x k + 1
150 fveq2 n = k G x n = G x k
151 149 150 oveq12d n = k G x n + 1 G x n = G x k + 1 G x k
152 151 fveq2d n = k G x n + 1 G x n = G x k + 1 G x k
153 152 cbvmptv n Z G x n + 1 G x n = k Z G x k + 1 G x k
154 5 reseq2i n 0 G x n + 1 G x n Z = n 0 G x n + 1 G x n M
155 26 adantr φ x 0 Z 0
156 155 resmptd φ x 0 n 0 G x n + 1 G x n Z = n Z G x n + 1 G x n
157 154 156 eqtr3id φ x 0 n 0 G x n + 1 G x n M = n Z G x n + 1 G x n
158 12 adantr φ x 0 M
159 8 adantr φ x 0 D L
160 137 abscld φ x 0 x
161 160 recnd φ x 0 x
162 14 mptex n 0 G x n + 1 G x n V
163 162 a1i φ x 0 n 0 G x n + 1 G x n V
164 73 recnd φ k Z D k
165 164 adantlr φ x 0 k Z D k
166 eqidd φ x 0 k Z n 0 G x n + 1 G x n = n 0 G x n + 1 G x n
167 152 adantl φ x 0 k Z n = k G x n + 1 G x n = G x k + 1 G x k
168 fvexd φ x 0 k Z G x k + 1 G x k V
169 166 167 139 168 fvmptd φ x 0 k Z n 0 G x n + 1 G x n k = G x k + 1 G x k
170 117 adantr φ x k Z G x = n 0 A n x n
171 simpr φ x k Z n = k + 1 n = k + 1
172 171 fveq2d φ x k Z n = k + 1 A n = A k + 1
173 171 oveq2d φ x k Z n = k + 1 x n = x k + 1
174 172 173 oveq12d φ x k Z n = k + 1 A n x n = A k + 1 x k + 1
175 1nn0 1 0
176 175 a1i φ x k Z 1 0
177 133 176 nn0addcld φ x k Z k + 1 0
178 ovexd φ x k Z A k + 1 x k + 1 V
179 170 174 177 178 fvmptd φ x k Z G x k + 1 = A k + 1 x k + 1
180 121 adantl φ x k Z n = k A n x n = A k x k
181 ovexd φ x k Z A k x k V
182 170 180 133 181 fvmptd φ x k Z G x k = A k x k
183 179 182 oveq12d φ x k Z G x k + 1 G x k = A k + 1 x k + 1 A k x k
184 113 183 sylanl2 φ x 0 k Z G x k + 1 G x k = A k + 1 x k + 1 A k x k
185 35 adantlr φ x 0 k Z A k + 1
186 113 177 sylanl2 φ x 0 k Z k + 1 0
187 138 186 expcld φ x 0 k Z x k + 1
188 185 136 187 140 141 145 divmuldivd φ x 0 k Z A k + 1 A k x k + 1 x k = A k + 1 x k + 1 A k x k
189 139 nn0cnd φ x 0 k Z k
190 1cnd φ x 0 k Z 1
191 189 190 pncan2d φ x 0 k Z k + 1 - k = 1
192 191 oveq2d φ x 0 k Z x k + 1 - k = x 1
193 186 nn0zd φ x 0 k Z k + 1
194 138 143 144 193 expsubd φ x 0 k Z x k + 1 - k = x k + 1 x k
195 138 exp1d φ x 0 k Z x 1 = x
196 192 194 195 3eqtr3d φ x 0 k Z x k + 1 x k = x
197 196 oveq2d φ x 0 k Z A k + 1 A k x k + 1 x k = A k + 1 A k x
198 184 188 197 3eqtr2d φ x 0 k Z G x k + 1 G x k = A k + 1 A k x
199 198 fveq2d φ x 0 k Z G x k + 1 G x k = A k + 1 A k x
200 39 adantlr φ x 0 k Z A k + 1 A k
201 200 138 absmuld φ x 0 k Z A k + 1 A k x = A k + 1 A k x
202 169 199 201 3eqtrd φ x 0 k Z n 0 G x n + 1 G x n k = A k + 1 A k x
203 72 30 eqtr3d φ k Z D k = A k + 1 A k
204 203 adantlr φ x 0 k Z D k = A k + 1 A k
205 204 eqcomd φ x 0 k Z A k + 1 A k = D k
206 205 oveq1d φ x 0 k Z A k + 1 A k x = D k x
207 161 adantr φ x 0 k Z x
208 165 207 mulcomd φ x 0 k Z D k x = x D k
209 202 206 208 3eqtrd φ x 0 k Z n 0 G x n + 1 G x n k = x D k
210 5 158 159 161 163 165 209 climmulc2 φ x 0 n 0 G x n + 1 G x n x L
211 climres M n 0 G x n + 1 G x n V n 0 G x n + 1 G x n M x L n 0 G x n + 1 G x n x L
212 158 162 211 sylancl φ x 0 n 0 G x n + 1 G x n M x L n 0 G x n + 1 G x n x L
213 210 212 mpbird φ x 0 n 0 G x n + 1 G x n M x L
214 157 213 eqbrtrrd φ x 0 n Z G x n + 1 G x n x L
215 214 adantr φ x 0 x L 1 n Z G x n + 1 G x n x L
216 simpr φ x 0 x L 1 x L 1
217 110 5 111 112 132 148 153 215 216 cvgdvgrat φ x 0 x L 1 x L < 1 seq 0 + G x dom
218 109 217 sylanl2 φ x 0 x L 1 x L < 1 seq 0 + G x dom
219 eldifi x 0 x
220 fveq2 r = x G r = G x
221 220 seqeq3d r = x seq 0 + G r = seq 0 + G x
222 221 eleq1d r = x seq 0 + G r dom seq 0 + G x dom
223 222 elrab3 x x r | seq 0 + G r dom seq 0 + G x dom
224 219 223 syl x 0 x r | seq 0 + G r dom seq 0 + G x dom
225 224 ad2antlr φ x 0 x L 1 x r | seq 0 + G r dom seq 0 + G x dom
226 218 225 bitr4d φ x 0 x L 1 x L < 1 x r | seq 0 + G r dom
227 226 an32s φ x L 1 x 0 x L < 1 x r | seq 0 + G r dom
228 105 227 jaodan φ x L 1 x 0 x 0 x L < 1 x r | seq 0 + G r dom
229 86 228 sylan2br φ x L 1 x x L < 1 x r | seq 0 + G r dom
230 229 an32s φ x x L 1 x L < 1 x r | seq 0 + G r dom
231 82 230 bitr3d φ x x L 1 x < 1 L x r | seq 0 + G r dom
232 69 231 syldan φ x x 1 L x < 1 L x r | seq 0 + G r dom
233 232 notbid φ x x 1 L ¬ x < 1 L ¬ x r | seq 0 + G r dom
234 58 233 bitrd φ x x 1 L 1 L < x ¬ x r | seq 0 + G r dom
235 234 biimpd φ x x 1 L 1 L < x ¬ x r | seq 0 + G r dom
236 235 impancom φ x 1 L < x x 1 L ¬ x r | seq 0 + G r dom
237 52 236 mpd φ x 1 L < x ¬ x r | seq 0 + G r dom
238 237 ex φ x 1 L < x ¬ x r | seq 0 + G r dom
239 238 con2d φ x x r | seq 0 + G r dom ¬ 1 L < x
240 47 adantr φ x 1 L < x 1 L
241 simplr φ x 1 L < x x
242 50 adantr φ x 1 L < x x
243 simpr φ x 1 L < x 1 L < x
244 241 leabsd φ x 1 L < x x x
245 240 241 242 243 244 ltletrd φ x 1 L < x 1 L < x
246 245 ex φ x 1 L < x 1 L < x
247 239 246 nsyld φ x x r | seq 0 + G r dom ¬ 1 L < x
248 46 247 sylan2 φ x r | seq 0 + G r dom x r | seq 0 + G r dom ¬ 1 L < x
249 45 248 mpd φ x r | seq 0 + G r dom ¬ 1 L < x
250 43 renegcld φ 1 L
251 250 rexrd φ 1 L *
252 iooss1 1 L * 1 L x x 1 L 1 L 1 L
253 251 252 sylan φ 1 L x x 1 L 1 L 1 L
254 253 adantlr φ x * x < 1 L 1 L x x 1 L 1 L 1 L
255 eliooord k x 1 L x < k k < 1 L
256 255 simpld k x 1 L x < k
257 256 rgen k x 1 L x < k
258 ioon0 x * 1 L * x 1 L x < 1 L
259 44 258 sylan2 x * φ x 1 L x < 1 L
260 259 ancoms φ x * x 1 L x < 1 L
261 260 biimpar φ x * x < 1 L x 1 L
262 r19.2zb x 1 L k x 1 L x < k k x 1 L x < k
263 261 262 sylib φ x * x < 1 L k x 1 L x < k k x 1 L x < k
264 257 263 mpi φ x * x < 1 L k x 1 L x < k
265 264 anasss φ x * x < 1 L k x 1 L x < k
266 265 adantr φ x * x < 1 L 1 L x k x 1 L x < k
267 ssrexv x 1 L 1 L 1 L k x 1 L x < k k 1 L 1 L x < k
268 254 266 267 sylc φ x * x < 1 L 1 L x k 1 L 1 L x < k
269 simplr φ x * ¬ 1 L x x *
270 xrltnle x * 1 L * x < 1 L ¬ 1 L x
271 xrltle x * 1 L * x < 1 L x 1 L
272 270 271 sylbird x * 1 L * ¬ 1 L x x 1 L
273 251 272 sylan2 x * φ ¬ 1 L x x 1 L
274 273 ancoms φ x * ¬ 1 L x x 1 L
275 274 imp φ x * ¬ 1 L x x 1 L
276 iooss1 x * x 1 L 1 L 1 L x 1 L
277 269 275 276 syl2anc φ x * ¬ 1 L x 1 L 1 L x 1 L
278 277 sselda φ x * ¬ 1 L x k 1 L 1 L k x 1 L
279 278 256 syl φ x * ¬ 1 L x k 1 L 1 L x < k
280 279 ralrimiva φ x * ¬ 1 L x k 1 L 1 L x < k
281 42 78 recgt0d φ 0 < 1 L
282 43 43 281 281 addgt0d φ 0 < 1 L + 1 L
283 43 recnd φ 1 L
284 283 283 subnegd φ 1 L 1 L = 1 L + 1 L
285 282 284 breqtrrd φ 0 < 1 L 1 L
286 250 43 posdifd φ 1 L < 1 L 0 < 1 L 1 L
287 285 286 mpbird φ 1 L < 1 L
288 ioon0 1 L * 1 L * 1 L 1 L 1 L < 1 L
289 251 44 288 syl2anc φ 1 L 1 L 1 L < 1 L
290 287 289 mpbird φ 1 L 1 L
291 r19.2zb 1 L 1 L k 1 L 1 L x < k k 1 L 1 L x < k
292 290 291 sylib φ k 1 L 1 L x < k k 1 L 1 L x < k
293 292 ad2antrr φ x * ¬ 1 L x k 1 L 1 L x < k k 1 L 1 L x < k
294 280 293 mpd φ x * ¬ 1 L x k 1 L 1 L x < k
295 294 adantlrr φ x * x < 1 L ¬ 1 L x k 1 L 1 L x < k
296 268 295 pm2.61dan φ x * x < 1 L k 1 L 1 L x < k
297 elioo2 1 L * 1 L * x 1 L 1 L x 1 L < x x < 1 L
298 251 44 297 syl2anc φ x 1 L 1 L x 1 L < x x < 1 L
299 298 biimpa φ x 1 L 1 L x 1 L < x x < 1 L
300 simpr φ x x
301 300 47 absltd φ x x < 1 L 1 L < x x < 1 L
302 50 adantr φ x x < 1 L x
303 simpr φ x x < 1 L x < 1 L
304 302 303 ltned φ x x < 1 L x 1 L
305 232 biimpd φ x x 1 L x < 1 L x r | seq 0 + G r dom
306 305 impancom φ x x < 1 L x 1 L x r | seq 0 + G r dom
307 304 306 mpd φ x x < 1 L x r | seq 0 + G r dom
308 307 ex φ x x < 1 L x r | seq 0 + G r dom
309 301 308 sylbird φ x 1 L < x x < 1 L x r | seq 0 + G r dom
310 309 impr φ x 1 L < x x < 1 L x r | seq 0 + G r dom
311 310 expcom x 1 L < x x < 1 L φ x r | seq 0 + G r dom
312 311 3impb x 1 L < x x < 1 L φ x r | seq 0 + G r dom
313 312 impcom φ x 1 L < x x < 1 L x r | seq 0 + G r dom
314 299 313 syldan φ x 1 L 1 L x r | seq 0 + G r dom
315 314 ex φ x 1 L 1 L x r | seq 0 + G r dom
316 315 ssrdv φ 1 L 1 L r | seq 0 + G r dom
317 ssrexv 1 L 1 L r | seq 0 + G r dom k 1 L 1 L x < k k r | seq 0 + G r dom x < k
318 316 317 syl φ k 1 L 1 L x < k k r | seq 0 + G r dom x < k
319 318 adantr φ x * x < 1 L k 1 L 1 L x < k k r | seq 0 + G r dom x < k
320 296 319 mpd φ x * x < 1 L k r | seq 0 + G r dom x < k
321 11 44 249 320 eqsupd φ sup r | seq 0 + G r dom * < = 1 L
322 3 321 syl5eq φ R = 1 L