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 = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
pserf.f 
|- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
pserf.a 
|- ( ph -> A : NN0 --> CC )
pserf.r 
|- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
psercn.s 
|- S = ( `' abs " ( 0 [,) R ) )
psercn.m 
|- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )
pserdv.b 
|- B = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) )
Assertion pserdv2 
|- ( ph -> ( CC _D F ) = ( y e. S |-> sum_ k e. NN ( ( k x. ( A ` k ) ) x. ( y ^ ( k - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pserf.g 
 |-  G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2 pserf.f 
 |-  F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
3 pserf.a 
 |-  ( ph -> A : NN0 --> CC )
4 pserf.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
5 psercn.s 
 |-  S = ( `' abs " ( 0 [,) R ) )
6 psercn.m 
 |-  M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )
7 pserdv.b 
 |-  B = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) )
8 1 2 3 4 5 6 7 pserdv 
 |-  ( ph -> ( CC _D F ) = ( y e. S |-> sum_ m e. NN0 ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( y ^ m ) ) ) )
9 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
10 nnuz 
 |-  NN = ( ZZ>= ` 1 )
11 1e0p1 
 |-  1 = ( 0 + 1 )
12 11 fveq2i 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
13 10 12 eqtri 
 |-  NN = ( ZZ>= ` ( 0 + 1 ) )
14 id 
 |-  ( k = ( 1 + m ) -> k = ( 1 + m ) )
15 fveq2 
 |-  ( k = ( 1 + m ) -> ( A ` k ) = ( A ` ( 1 + m ) ) )
16 14 15 oveq12d 
 |-  ( k = ( 1 + m ) -> ( k x. ( A ` k ) ) = ( ( 1 + m ) x. ( A ` ( 1 + m ) ) ) )
17 oveq1 
 |-  ( k = ( 1 + m ) -> ( k - 1 ) = ( ( 1 + m ) - 1 ) )
18 17 oveq2d 
 |-  ( k = ( 1 + m ) -> ( y ^ ( k - 1 ) ) = ( y ^ ( ( 1 + m ) - 1 ) ) )
19 16 18 oveq12d 
 |-  ( k = ( 1 + m ) -> ( ( k x. ( A ` k ) ) x. ( y ^ ( k - 1 ) ) ) = ( ( ( 1 + m ) x. ( A ` ( 1 + m ) ) ) x. ( y ^ ( ( 1 + m ) - 1 ) ) ) )
20 1zzd 
 |-  ( ( ph /\ y e. S ) -> 1 e. ZZ )
21 0zd 
 |-  ( ( ph /\ y e. S ) -> 0 e. ZZ )
22 nncn 
 |-  ( k e. NN -> k e. CC )
23 22 adantl 
 |-  ( ( ( ph /\ y e. S ) /\ k e. NN ) -> k e. CC )
24 3 adantr 
 |-  ( ( ph /\ y e. S ) -> A : NN0 --> CC )
25 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
26 ffvelrn 
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
27 24 25 26 syl2an 
 |-  ( ( ( ph /\ y e. S ) /\ k e. NN ) -> ( A ` k ) e. CC )
28 23 27 mulcld 
 |-  ( ( ( ph /\ y e. S ) /\ k e. NN ) -> ( k x. ( A ` k ) ) e. CC )
29 cnvimass 
 |-  ( `' abs " ( 0 [,) R ) ) C_ dom abs
30 absf 
 |-  abs : CC --> RR
31 30 fdmi 
 |-  dom abs = CC
32 29 31 sseqtri 
 |-  ( `' abs " ( 0 [,) R ) ) C_ CC
33 5 32 eqsstri 
 |-  S C_ CC
34 33 a1i 
 |-  ( ph -> S C_ CC )
35 34 sselda 
 |-  ( ( ph /\ y e. S ) -> y e. CC )
36 nnm1nn0 
 |-  ( k e. NN -> ( k - 1 ) e. NN0 )
37 expcl 
 |-  ( ( y e. CC /\ ( k - 1 ) e. NN0 ) -> ( y ^ ( k - 1 ) ) e. CC )
38 35 36 37 syl2an 
 |-  ( ( ( ph /\ y e. S ) /\ k e. NN ) -> ( y ^ ( k - 1 ) ) e. CC )
39 28 38 mulcld 
 |-  ( ( ( ph /\ y e. S ) /\ k e. NN ) -> ( ( k x. ( A ` k ) ) x. ( y ^ ( k - 1 ) ) ) e. CC )
40 9 13 19 20 21 39 isumshft 
 |-  ( ( ph /\ y e. S ) -> sum_ k e. NN ( ( k x. ( A ` k ) ) x. ( y ^ ( k - 1 ) ) ) = sum_ m e. NN0 ( ( ( 1 + m ) x. ( A ` ( 1 + m ) ) ) x. ( y ^ ( ( 1 + m ) - 1 ) ) ) )
41 ax-1cn 
 |-  1 e. CC
42 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
43 42 adantl 
 |-  ( ( ( ph /\ y e. S ) /\ m e. NN0 ) -> m e. CC )
44 addcom 
 |-  ( ( 1 e. CC /\ m e. CC ) -> ( 1 + m ) = ( m + 1 ) )
45 41 43 44 sylancr 
 |-  ( ( ( ph /\ y e. S ) /\ m e. NN0 ) -> ( 1 + m ) = ( m + 1 ) )
46 45 fveq2d 
 |-  ( ( ( ph /\ y e. S ) /\ m e. NN0 ) -> ( A ` ( 1 + m ) ) = ( A ` ( m + 1 ) ) )
47 45 46 oveq12d 
 |-  ( ( ( ph /\ y e. S ) /\ m e. NN0 ) -> ( ( 1 + m ) x. ( A ` ( 1 + m ) ) ) = ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) )
48 pncan2 
 |-  ( ( 1 e. CC /\ m e. CC ) -> ( ( 1 + m ) - 1 ) = m )
49 41 43 48 sylancr 
 |-  ( ( ( ph /\ y e. S ) /\ m e. NN0 ) -> ( ( 1 + m ) - 1 ) = m )
50 49 oveq2d 
 |-  ( ( ( ph /\ y e. S ) /\ m e. NN0 ) -> ( y ^ ( ( 1 + m ) - 1 ) ) = ( y ^ m ) )
51 47 50 oveq12d 
 |-  ( ( ( ph /\ y e. S ) /\ m e. NN0 ) -> ( ( ( 1 + m ) x. ( A ` ( 1 + m ) ) ) x. ( y ^ ( ( 1 + m ) - 1 ) ) ) = ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( y ^ m ) ) )
52 51 sumeq2dv 
 |-  ( ( ph /\ y e. S ) -> sum_ m e. NN0 ( ( ( 1 + m ) x. ( A ` ( 1 + m ) ) ) x. ( y ^ ( ( 1 + m ) - 1 ) ) ) = sum_ m e. NN0 ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( y ^ m ) ) )
53 40 52 eqtr2d 
 |-  ( ( ph /\ y e. S ) -> sum_ m e. NN0 ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( y ^ m ) ) = sum_ k e. NN ( ( k x. ( A ` k ) ) x. ( y ^ ( k - 1 ) ) ) )
54 53 mpteq2dva 
 |-  ( ph -> ( y e. S |-> sum_ m e. NN0 ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( y ^ m ) ) ) = ( y e. S |-> sum_ k e. NN ( ( k x. ( A ` k ) ) x. ( y ^ ( k - 1 ) ) ) ) )
55 8 54 eqtrd 
 |-  ( ph -> ( CC _D F ) = ( y e. S |-> sum_ k e. NN ( ( k x. ( A ` k ) ) x. ( y ^ ( k - 1 ) ) ) ) )