Description: The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pserf.g | |
|
pserf.f | |
||
pserf.a | |
||
pserf.r | |
||
psercn.s | |
||
psercn.m | |
||
pserdv.b | |
||
Assertion | pserdv2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pserf.g | |
|
2 | pserf.f | |
|
3 | pserf.a | |
|
4 | pserf.r | |
|
5 | psercn.s | |
|
6 | psercn.m | |
|
7 | pserdv.b | |
|
8 | 1 2 3 4 5 6 7 | pserdv | |
9 | nn0uz | |
|
10 | nnuz | |
|
11 | 1e0p1 | |
|
12 | 11 | fveq2i | |
13 | 10 12 | eqtri | |
14 | id | |
|
15 | fveq2 | |
|
16 | 14 15 | oveq12d | |
17 | oveq1 | |
|
18 | 17 | oveq2d | |
19 | 16 18 | oveq12d | |
20 | 1zzd | |
|
21 | 0zd | |
|
22 | nncn | |
|
23 | 22 | adantl | |
24 | 3 | adantr | |
25 | nnnn0 | |
|
26 | ffvelcdm | |
|
27 | 24 25 26 | syl2an | |
28 | 23 27 | mulcld | |
29 | cnvimass | |
|
30 | absf | |
|
31 | 30 | fdmi | |
32 | 29 31 | sseqtri | |
33 | 5 32 | eqsstri | |
34 | 33 | a1i | |
35 | 34 | sselda | |
36 | nnm1nn0 | |
|
37 | expcl | |
|
38 | 35 36 37 | syl2an | |
39 | 28 38 | mulcld | |
40 | 9 13 19 20 21 39 | isumshft | |
41 | ax-1cn | |
|
42 | nn0cn | |
|
43 | 42 | adantl | |
44 | addcom | |
|
45 | 41 43 44 | sylancr | |
46 | 45 | fveq2d | |
47 | 45 46 | oveq12d | |
48 | pncan2 | |
|
49 | 41 43 48 | sylancr | |
50 | 49 | oveq2d | |
51 | 47 50 | oveq12d | |
52 | 51 | sumeq2dv | |
53 | 40 52 | eqtr2d | |
54 | 53 | mpteq2dva | |
55 | 8 54 | eqtrd | |