Metamath Proof Explorer

Theorem pserdv

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 pserdv 
|- ( ph -> ( CC _D F ) = ( y e. S |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )

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 dvfcn 
 |-  ( CC _D F ) : dom ( CC _D F ) --> CC
9 ssidd 
 |-  ( ph -> CC C_ CC )
10 1 2 3 4 5 6 psercn 
 |-  ( ph -> F e. ( S -cn-> CC ) )
11 cncff 
 |-  ( F e. ( S -cn-> CC ) -> F : S --> CC )
12 10 11 syl 
 |-  ( ph -> F : S --> CC )
13 cnvimass 
 |-  ( `' abs " ( 0 [,) R ) ) C_ dom abs
14 absf 
 |-  abs : CC --> RR
15 14 fdmi 
 |-  dom abs = CC
16 13 15 sseqtri 
 |-  ( `' abs " ( 0 [,) R ) ) C_ CC
17 5 16 eqsstri 
 |-  S C_ CC
18 17 a1i 
 |-  ( ph -> S C_ CC )
19 9 12 18 dvbss 
 |-  ( ph -> dom ( CC _D F ) C_ S )
20 ssidd 
 |-  ( ( ph /\ a e. S ) -> CC C_ CC )
21 12 adantr 
 |-  ( ( ph /\ a e. S ) -> F : S --> CC )
22 17 a1i 
 |-  ( ( ph /\ a e. S ) -> S C_ CC )
23 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
24 0cnd 
 |-  ( ( ph /\ a e. S ) -> 0 e. CC )
25 18 sselda 
 |-  ( ( ph /\ a e. S ) -> a e. CC )
26 25 abscld 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) e. RR )
27 1 2 3 4 5 6 psercnlem1 
 |-  ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) )
28 27 simp1d 
 |-  ( ( ph /\ a e. S ) -> M e. RR+ )
29 28 rpred 
 |-  ( ( ph /\ a e. S ) -> M e. RR )
30 26 29 readdcld 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) + M ) e. RR )
31 0red 
 |-  ( ( ph /\ a e. S ) -> 0 e. RR )
32 25 absge0d 
 |-  ( ( ph /\ a e. S ) -> 0 <_ ( abs ` a ) )
33 26 28 ltaddrpd 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < ( ( abs ` a ) + M ) )
34 31 26 30 32 33 lelttrd 
 |-  ( ( ph /\ a e. S ) -> 0 < ( ( abs ` a ) + M ) )
35 30 34 elrpd 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) + M ) e. RR+ )
36 35 rphalfcld 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR+ )
37 36 rpxrd 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR* )
38 blssm 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ ( ( ( abs ` a ) + M ) / 2 ) e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) C_ CC )
39 23 24 37 38 mp3an2i 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) C_ CC )
40 7 39 eqsstrid 
 |-  ( ( ph /\ a e. S ) -> B C_ CC )
41 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
42 41 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
43 42 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
44 41 43 dvres 
 |-  ( ( ( CC C_ CC /\ F : S --> CC ) /\ ( S C_ CC /\ B C_ CC ) ) -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` B ) ) )
45 20 21 22 40 44 syl22anc 
 |-  ( ( ph /\ a e. S ) -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` B ) ) )
46 resss 
 |-  ( ( CC _D F ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` B ) ) C_ ( CC _D F )
47 45 46 eqsstrdi 
 |-  ( ( ph /\ a e. S ) -> ( CC _D ( F |` B ) ) C_ ( CC _D F ) )
48 dmss 
 |-  ( ( CC _D ( F |` B ) ) C_ ( CC _D F ) -> dom ( CC _D ( F |` B ) ) C_ dom ( CC _D F ) )
49 47 48 syl 
 |-  ( ( ph /\ a e. S ) -> dom ( CC _D ( F |` B ) ) C_ dom ( CC _D F ) )
50 1 2 3 4 5 6 pserdvlem1 
 |-  ( ( ph /\ a e. S ) -> ( ( ( ( abs ` a ) + M ) / 2 ) e. RR+ /\ ( abs ` a ) < ( ( ( abs ` a ) + M ) / 2 ) /\ ( ( ( abs ` a ) + M ) / 2 ) < R ) )
51 1 2 3 4 5 50 psercnlem2 
 |-  ( ( ph /\ a e. S ) -> ( a e. ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) /\ ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) C_ ( `' abs " ( 0 [,] ( ( ( abs ` a ) + M ) / 2 ) ) ) /\ ( `' abs " ( 0 [,] ( ( ( abs ` a ) + M ) / 2 ) ) ) C_ S ) )
52 51 simp1d 
 |-  ( ( ph /\ a e. S ) -> a e. ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) )
53 52 7 eleqtrrdi 
 |-  ( ( ph /\ a e. S ) -> a e. B )
54 1 2 3 4 5 6 7 pserdvlem2 
 |-  ( ( ph /\ a e. S ) -> ( CC _D ( F |` B ) ) = ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
55 54 dmeqd 
 |-  ( ( ph /\ a e. S ) -> dom ( CC _D ( F |` B ) ) = dom ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
56 dmmptg 
 |-  ( A. y e. B sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) e. _V -> dom ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) = B )
57 sumex 
 |-  sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) e. _V
58 57 a1i 
 |-  ( y e. B -> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) e. _V )
59 56 58 mprg 
 |-  dom ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) = B
60 55 59 eqtrdi 
 |-  ( ( ph /\ a e. S ) -> dom ( CC _D ( F |` B ) ) = B )
61 53 60 eleqtrrd 
 |-  ( ( ph /\ a e. S ) -> a e. dom ( CC _D ( F |` B ) ) )
62 49 61 sseldd 
 |-  ( ( ph /\ a e. S ) -> a e. dom ( CC _D F ) )
63 19 62 eqelssd 
 |-  ( ph -> dom ( CC _D F ) = S )
64 63 feq2d 
 |-  ( ph -> ( ( CC _D F ) : dom ( CC _D F ) --> CC <-> ( CC _D F ) : S --> CC ) )
65 8 64 mpbii 
 |-  ( ph -> ( CC _D F ) : S --> CC )
66 65 feqmptd 
 |-  ( ph -> ( CC _D F ) = ( a e. S |-> ( ( CC _D F ) ` a ) ) )
67 ffun 
 |-  ( ( CC _D F ) : dom ( CC _D F ) --> CC -> Fun ( CC _D F ) )
68 8 67 mp1i 
 |-  ( ( ph /\ a e. S ) -> Fun ( CC _D F ) )
69 funssfv 
 |-  ( ( Fun ( CC _D F ) /\ ( CC _D ( F |` B ) ) C_ ( CC _D F ) /\ a e. dom ( CC _D ( F |` B ) ) ) -> ( ( CC _D F ) ` a ) = ( ( CC _D ( F |` B ) ) ` a ) )
70 68 47 61 69 syl3anc 
 |-  ( ( ph /\ a e. S ) -> ( ( CC _D F ) ` a ) = ( ( CC _D ( F |` B ) ) ` a ) )
71 54 fveq1d 
 |-  ( ( ph /\ a e. S ) -> ( ( CC _D ( F |` B ) ) ` a ) = ( ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) ` a ) )
72 oveq1 
 |-  ( y = a -> ( y ^ k ) = ( a ^ k ) )
73 72 oveq2d 
 |-  ( y = a -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) )
74 73 sumeq2sdv 
 |-  ( y = a -> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) = sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) )
75 eqid 
 |-  ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) = ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
76 sumex 
 |-  sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) e. _V
77 74 75 76 fvmpt 
 |-  ( a e. B -> ( ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) ` a ) = sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) )
78 53 77 syl 
 |-  ( ( ph /\ a e. S ) -> ( ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) ` a ) = sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) )
79 70 71 78 3eqtrd 
 |-  ( ( ph /\ a e. S ) -> ( ( CC _D F ) ` a ) = sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) )
80 79 mpteq2dva 
 |-  ( ph -> ( a e. S |-> ( ( CC _D F ) ` a ) ) = ( a e. S |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) ) )
81 66 80 eqtrd 
 |-  ( ph -> ( CC _D F ) = ( a e. S |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) ) )
82 oveq1 
 |-  ( a = y -> ( a ^ k ) = ( y ^ k ) )
83 82 oveq2d 
 |-  ( a = y -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
84 83 sumeq2sdv 
 |-  ( a = y -> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) = sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
85 84 cbvmptv 
 |-  ( a e. S |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( a ^ k ) ) ) = ( y e. S |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
86 81 85 eqtrdi 
 |-  ( ph -> ( CC _D F ) = ( y e. S |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )