Metamath Proof Explorer


Theorem dvradcnv

Description: The radius of convergence of the (formal) derivative H of the power series G is at least as large as the radius of convergence of G . (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses dvradcnv.g G = x n 0 A n x n
dvradcnv.r R = sup r | seq 0 + G r dom * <
dvradcnv.h H = n 0 n + 1 A n + 1 X n
dvradcnv.a φ A : 0
dvradcnv.x φ X
dvradcnv.l φ X < R
Assertion dvradcnv φ seq 0 + H dom

Proof

Step Hyp Ref Expression
1 dvradcnv.g G = x n 0 A n x n
2 dvradcnv.r R = sup r | seq 0 + G r dom * <
3 dvradcnv.h H = n 0 n + 1 A n + 1 X n
4 dvradcnv.a φ A : 0
5 dvradcnv.x φ X
6 dvradcnv.l φ X < R
7 nn0uz 0 = 0
8 1nn0 1 0
9 8 a1i φ 1 0
10 ax-1cn 1
11 nn0cn k 0 k
12 11 adantl φ k 0 k
13 nn0ex 0 V
14 13 mptex i 0 i G X i V
15 14 shftval4 1 k i 0 i G X i shift -1 k = i 0 i G X i 1 + k
16 10 12 15 sylancr φ k 0 i 0 i G X i shift -1 k = i 0 i G X i 1 + k
17 addcom 1 k 1 + k = k + 1
18 10 12 17 sylancr φ k 0 1 + k = k + 1
19 18 fveq2d φ k 0 i 0 i G X i 1 + k = i 0 i G X i k + 1
20 peano2nn0 k 0 k + 1 0
21 20 adantl φ k 0 k + 1 0
22 id i = k + 1 i = k + 1
23 2fveq3 i = k + 1 G X i = G X k + 1
24 22 23 oveq12d i = k + 1 i G X i = k + 1 G X k + 1
25 eqid i 0 i G X i = i 0 i G X i
26 ovex k + 1 G X k + 1 V
27 24 25 26 fvmpt k + 1 0 i 0 i G X i k + 1 = k + 1 G X k + 1
28 21 27 syl φ k 0 i 0 i G X i k + 1 = k + 1 G X k + 1
29 1 pserval2 X k + 1 0 G X k + 1 = A k + 1 X k + 1
30 5 20 29 syl2an φ k 0 G X k + 1 = A k + 1 X k + 1
31 30 fveq2d φ k 0 G X k + 1 = A k + 1 X k + 1
32 31 oveq2d φ k 0 k + 1 G X k + 1 = k + 1 A k + 1 X k + 1
33 28 32 eqtrd φ k 0 i 0 i G X i k + 1 = k + 1 A k + 1 X k + 1
34 16 19 33 3eqtrd φ k 0 i 0 i G X i shift -1 k = k + 1 A k + 1 X k + 1
35 21 nn0red φ k 0 k + 1
36 ffvelrn A : 0 k + 1 0 A k + 1
37 4 20 36 syl2an φ k 0 A k + 1
38 expcl X k + 1 0 X k + 1
39 5 20 38 syl2an φ k 0 X k + 1
40 37 39 mulcld φ k 0 A k + 1 X k + 1
41 40 abscld φ k 0 A k + 1 X k + 1
42 35 41 remulcld φ k 0 k + 1 A k + 1 X k + 1
43 34 42 eqeltrd φ k 0 i 0 i G X i shift -1 k
44 oveq1 n = k n + 1 = k + 1
45 44 fveq2d n = k A n + 1 = A k + 1
46 44 45 oveq12d n = k n + 1 A n + 1 = k + 1 A k + 1
47 oveq2 n = k X n = X k
48 46 47 oveq12d n = k n + 1 A n + 1 X n = k + 1 A k + 1 X k
49 ovex k + 1 A k + 1 X k V
50 48 3 49 fvmpt k 0 H k = k + 1 A k + 1 X k
51 50 adantl φ k 0 H k = k + 1 A k + 1 X k
52 21 nn0cnd φ k 0 k + 1
53 52 37 mulcld φ k 0 k + 1 A k + 1
54 expcl X k 0 X k
55 5 54 sylan φ k 0 X k
56 53 55 mulcld φ k 0 k + 1 A k + 1 X k
57 51 56 eqeltrd φ k 0 H k
58 id i = k i = k
59 2fveq3 i = k G X i = G X k
60 58 59 oveq12d i = k i G X i = k G X k
61 60 cbvmptv i 0 i G X i = k 0 k G X k
62 1 4 2 5 6 61 radcnvlt1 φ seq 0 + i 0 i G X i dom seq 0 + abs G X dom
63 62 simpld φ seq 0 + i 0 i G X i dom
64 climdm seq 0 + i 0 i G X i dom seq 0 + i 0 i G X i seq 0 + i 0 i G X i
65 63 64 sylib φ seq 0 + i 0 i G X i seq 0 + i 0 i G X i
66 0z 0
67 neg1z 1
68 14 isershft 0 1 seq 0 + i 0 i G X i seq 0 + i 0 i G X i seq 0 + -1 + i 0 i G X i shift -1 seq 0 + i 0 i G X i
69 66 67 68 mp2an seq 0 + i 0 i G X i seq 0 + i 0 i G X i seq 0 + -1 + i 0 i G X i shift -1 seq 0 + i 0 i G X i
70 65 69 sylib φ seq 0 + -1 + i 0 i G X i shift -1 seq 0 + i 0 i G X i
71 seqex seq 0 + -1 + i 0 i G X i shift -1 V
72 fvex seq 0 + i 0 i G X i V
73 71 72 breldm seq 0 + -1 + i 0 i G X i shift -1 seq 0 + i 0 i G X i seq 0 + -1 + i 0 i G X i shift -1 dom
74 70 73 syl φ seq 0 + -1 + i 0 i G X i shift -1 dom
75 eqid 0 + -1 = 0 + -1
76 neg1cn 1
77 76 addid2i 0 + -1 = 1
78 0le1 0 1
79 1re 1
80 le0neg2 1 0 1 1 0
81 79 80 ax-mp 0 1 1 0
82 78 81 mpbi 1 0
83 77 82 eqbrtri 0 + -1 0
84 77 67 eqeltri 0 + -1
85 84 eluz1i 0 0 + -1 0 0 + -1 0
86 66 83 85 mpbir2an 0 0 + -1
87 86 a1i φ 0 0 + -1
88 eluzelcn k 0 + -1 k
89 88 adantl φ k 0 + -1 k
90 10 89 15 sylancr φ k 0 + -1 i 0 i G X i shift -1 k = i 0 i G X i 1 + k
91 nn0re i 0 i
92 91 adantl φ i 0 i
93 1 4 5 psergf φ G X : 0
94 93 ffvelrnda φ i 0 G X i
95 94 abscld φ i 0 G X i
96 92 95 remulcld φ i 0 i G X i
97 96 recnd φ i 0 i G X i
98 97 fmpttd φ i 0 i G X i : 0
99 10 88 17 sylancr k 0 + -1 1 + k = k + 1
100 eluzp1p1 k 0 + -1 k + 1 0 + -1 + 1
101 77 oveq1i 0 + -1 + 1 = - 1 + 1
102 1pneg1e0 1 + -1 = 0
103 10 76 102 addcomli - 1 + 1 = 0
104 101 103 eqtri 0 + -1 + 1 = 0
105 104 fveq2i 0 + -1 + 1 = 0
106 7 105 eqtr4i 0 = 0 + -1 + 1
107 100 106 eleqtrrdi k 0 + -1 k + 1 0
108 99 107 eqeltrd k 0 + -1 1 + k 0
109 ffvelrn i 0 i G X i : 0 1 + k 0 i 0 i G X i 1 + k
110 98 108 109 syl2an φ k 0 + -1 i 0 i G X i 1 + k
111 90 110 eqeltrd φ k 0 + -1 i 0 i G X i shift -1 k
112 75 87 111 iserex φ seq 0 + -1 + i 0 i G X i shift -1 dom seq 0 + i 0 i G X i shift -1 dom
113 74 112 mpbid φ seq 0 + i 0 i G X i shift -1 dom
114 1red φ X = 0 1
115 neqne ¬ X = 0 X 0
116 absrpcl X X 0 X +
117 5 115 116 syl2an φ ¬ X = 0 X +
118 117 rprecred φ ¬ X = 0 1 X
119 114 118 ifclda φ if X = 0 1 1 X
120 oveq1 1 = if X = 0 1 1 X 1 k + 1 A k + 1 X k + 1 = if X = 0 1 1 X k + 1 A k + 1 X k + 1
121 120 breq2d 1 = if X = 0 1 1 X k + 1 A k + 1 X k 1 k + 1 A k + 1 X k + 1 k + 1 A k + 1 X k if X = 0 1 1 X k + 1 A k + 1 X k + 1
122 oveq1 1 X = if X = 0 1 1 X 1 X k + 1 A k + 1 X k + 1 = if X = 0 1 1 X k + 1 A k + 1 X k + 1
123 122 breq2d 1 X = if X = 0 1 1 X k + 1 A k + 1 X k 1 X k + 1 A k + 1 X k + 1 k + 1 A k + 1 X k if X = 0 1 1 X k + 1 A k + 1 X k + 1
124 elnnuz k k 1
125 nnnn0 k k 0
126 124 125 sylbir k 1 k 0
127 21 nn0ge0d φ k 0 0 k + 1
128 40 absge0d φ k 0 0 A k + 1 X k + 1
129 35 41 127 128 mulge0d φ k 0 0 k + 1 A k + 1 X k + 1
130 126 129 sylan2 φ k 1 0 k + 1 A k + 1 X k + 1
131 130 adantr φ k 1 X = 0 0 k + 1 A k + 1 X k + 1
132 oveq1 X = 0 X k = 0 k
133 simpr φ k 1 k 1
134 133 124 sylibr φ k 1 k
135 134 0expd φ k 1 0 k = 0
136 132 135 sylan9eqr φ k 1 X = 0 X k = 0
137 136 oveq2d φ k 1 X = 0 k + 1 A k + 1 X k = k + 1 A k + 1 0
138 53 mul01d φ k 0 k + 1 A k + 1 0 = 0
139 126 138 sylan2 φ k 1 k + 1 A k + 1 0 = 0
140 139 adantr φ k 1 X = 0 k + 1 A k + 1 0 = 0
141 137 140 eqtrd φ k 1 X = 0 k + 1 A k + 1 X k = 0
142 141 abs00bd φ k 1 X = 0 k + 1 A k + 1 X k = 0
143 42 recnd φ k 0 k + 1 A k + 1 X k + 1
144 143 mulid2d φ k 0 1 k + 1 A k + 1 X k + 1 = k + 1 A k + 1 X k + 1
145 126 144 sylan2 φ k 1 1 k + 1 A k + 1 X k + 1 = k + 1 A k + 1 X k + 1
146 145 adantr φ k 1 X = 0 1 k + 1 A k + 1 X k + 1 = k + 1 A k + 1 X k + 1
147 131 142 146 3brtr4d φ k 1 X = 0 k + 1 A k + 1 X k 1 k + 1 A k + 1 X k + 1
148 df-ne X 0 ¬ X = 0
149 56 abscld φ k 0 k + 1 A k + 1 X k
150 52 37 55 mulassd φ k 0 k + 1 A k + 1 X k = k + 1 A k + 1 X k
151 150 fveq2d φ k 0 k + 1 A k + 1 X k = k + 1 A k + 1 X k
152 37 55 mulcld φ k 0 A k + 1 X k
153 52 152 absmuld φ k 0 k + 1 A k + 1 X k = k + 1 A k + 1 X k
154 35 127 absidd φ k 0 k + 1 = k + 1
155 154 oveq1d φ k 0 k + 1 A k + 1 X k = k + 1 A k + 1 X k
156 151 153 155 3eqtrd φ k 0 k + 1 A k + 1 X k = k + 1 A k + 1 X k
157 149 156 eqled φ k 0 k + 1 A k + 1 X k k + 1 A k + 1 X k
158 157 adantr φ k 0 X 0 k + 1 A k + 1 X k k + 1 A k + 1 X k
159 5 adantr φ k 0 X
160 116 rpreccld X X 0 1 X +
161 159 160 sylan φ k 0 X 0 1 X +
162 161 rpcnd φ k 0 X 0 1 X
163 52 adantr φ k 0 X 0 k + 1
164 41 adantr φ k 0 X 0 A k + 1 X k + 1
165 164 recnd φ k 0 X 0 A k + 1 X k + 1
166 162 163 165 mul12d φ k 0 X 0 1 X k + 1 A k + 1 X k + 1 = k + 1 1 X A k + 1 X k + 1
167 40 adantr φ k 0 X 0 A k + 1 X k + 1
168 5 ad2antrr φ k 0 X 0 X
169 simpr φ k 0 X 0 X 0
170 167 168 169 absdivd φ k 0 X 0 A k + 1 X k + 1 X = A k + 1 X k + 1 X
171 37 adantr φ k 0 X 0 A k + 1
172 39 adantr φ k 0 X 0 X k + 1
173 171 172 168 169 divassd φ k 0 X 0 A k + 1 X k + 1 X = A k + 1 X k + 1 X
174 12 adantr φ k 0 X 0 k
175 pncan k 1 k + 1 - 1 = k
176 174 10 175 sylancl φ k 0 X 0 k + 1 - 1 = k
177 176 oveq2d φ k 0 X 0 X k + 1 - 1 = X k
178 21 nn0zd φ k 0 k + 1
179 178 adantr φ k 0 X 0 k + 1
180 168 169 179 expm1d φ k 0 X 0 X k + 1 - 1 = X k + 1 X
181 177 180 eqtr3d φ k 0 X 0 X k = X k + 1 X
182 181 oveq2d φ k 0 X 0 A k + 1 X k = A k + 1 X k + 1 X
183 173 182 eqtr4d φ k 0 X 0 A k + 1 X k + 1 X = A k + 1 X k
184 183 fveq2d φ k 0 X 0 A k + 1 X k + 1 X = A k + 1 X k
185 5 abscld φ X
186 185 ad2antrr φ k 0 X 0 X
187 186 recnd φ k 0 X 0 X
188 159 116 sylan φ k 0 X 0 X +
189 188 rpne0d φ k 0 X 0 X 0
190 165 187 189 divrec2d φ k 0 X 0 A k + 1 X k + 1 X = 1 X A k + 1 X k + 1
191 170 184 190 3eqtr3rd φ k 0 X 0 1 X A k + 1 X k + 1 = A k + 1 X k
192 191 oveq2d φ k 0 X 0 k + 1 1 X A k + 1 X k + 1 = k + 1 A k + 1 X k
193 166 192 eqtrd φ k 0 X 0 1 X k + 1 A k + 1 X k + 1 = k + 1 A k + 1 X k
194 158 193 breqtrrd φ k 0 X 0 k + 1 A k + 1 X k 1 X k + 1 A k + 1 X k + 1
195 126 194 sylanl2 φ k 1 X 0 k + 1 A k + 1 X k 1 X k + 1 A k + 1 X k + 1
196 148 195 sylan2br φ k 1 ¬ X = 0 k + 1 A k + 1 X k 1 X k + 1 A k + 1 X k + 1
197 121 123 147 196 ifbothda φ k 1 k + 1 A k + 1 X k if X = 0 1 1 X k + 1 A k + 1 X k + 1
198 51 fveq2d φ k 0 H k = k + 1 A k + 1 X k
199 126 198 sylan2 φ k 1 H k = k + 1 A k + 1 X k
200 34 oveq2d φ k 0 if X = 0 1 1 X i 0 i G X i shift -1 k = if X = 0 1 1 X k + 1 A k + 1 X k + 1
201 126 200 sylan2 φ k 1 if X = 0 1 1 X i 0 i G X i shift -1 k = if X = 0 1 1 X k + 1 A k + 1 X k + 1
202 197 199 201 3brtr4d φ k 1 H k if X = 0 1 1 X i 0 i G X i shift -1 k
203 7 9 43 57 113 119 202 cvgcmpce φ seq 0 + H dom