Metamath Proof Explorer


Theorem pserdv2

Description: The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses pserf.g G=xn0Anxn
pserf.f F=ySj0Gyj
pserf.a φA:0
pserf.r R=supr|seq0+Grdom*<
psercn.s S=abs-10R
psercn.m M=ifRa+R2a+1
pserdv.b B=0ballabsa+M2
Assertion pserdv2 φDF=ySkkAkyk1

Proof

Step Hyp Ref Expression
1 pserf.g G=xn0Anxn
2 pserf.f F=ySj0Gyj
3 pserf.a φA:0
4 pserf.r R=supr|seq0+Grdom*<
5 psercn.s S=abs-10R
6 psercn.m M=ifRa+R2a+1
7 pserdv.b B=0ballabsa+M2
8 1 2 3 4 5 6 7 pserdv φDF=ySm0m+1Am+1ym
9 nn0uz 0=0
10 nnuz =1
11 1e0p1 1=0+1
12 11 fveq2i 1=0+1
13 10 12 eqtri =0+1
14 id k=1+mk=1+m
15 fveq2 k=1+mAk=A1+m
16 14 15 oveq12d k=1+mkAk=1+mA1+m
17 oveq1 k=1+mk1=1+m-1
18 17 oveq2d k=1+myk1=y1+m-1
19 16 18 oveq12d k=1+mkAkyk1=1+mA1+my1+m-1
20 1zzd φyS1
21 0zd φyS0
22 nncn kk
23 22 adantl φySkk
24 3 adantr φySA:0
25 nnnn0 kk0
26 ffvelcdm A:0k0Ak
27 24 25 26 syl2an φySkAk
28 23 27 mulcld φySkkAk
29 cnvimass abs-10Rdomabs
30 absf abs:
31 30 fdmi domabs=
32 29 31 sseqtri abs-10R
33 5 32 eqsstri S
34 33 a1i φS
35 34 sselda φySy
36 nnm1nn0 kk10
37 expcl yk10yk1
38 35 36 37 syl2an φySkyk1
39 28 38 mulcld φySkkAkyk1
40 9 13 19 20 21 39 isumshft φySkkAkyk1=m01+mA1+my1+m-1
41 ax-1cn 1
42 nn0cn m0m
43 42 adantl φySm0m
44 addcom 1m1+m=m+1
45 41 43 44 sylancr φySm01+m=m+1
46 45 fveq2d φySm0A1+m=Am+1
47 45 46 oveq12d φySm01+mA1+m=m+1Am+1
48 pncan2 1m1+m-1=m
49 41 43 48 sylancr φySm01+m-1=m
50 49 oveq2d φySm0y1+m-1=ym
51 47 50 oveq12d φySm01+mA1+my1+m-1=m+1Am+1ym
52 51 sumeq2dv φySm01+mA1+my1+m-1=m0m+1Am+1ym
53 40 52 eqtr2d φySm0m+1Am+1ym=kkAkyk1
54 53 mpteq2dva φySm0m+1Am+1ym=ySkkAkyk1
55 8 54 eqtrd φDF=ySkkAkyk1