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 n 0 A n x n
pserf.f F = y S j 0 G y j
pserf.a φ A : 0
pserf.r R = sup r | seq 0 + G r dom * <
psercn.s S = abs -1 0 R
psercn.m M = if R a + R 2 a + 1
pserdv.b B = 0 ball abs a + M 2
Assertion pserdv φ D F = y S k 0 k + 1 A k + 1 y k

Proof

Step Hyp Ref Expression
1 pserf.g G = x n 0 A n x n
2 pserf.f F = y S j 0 G y j
3 pserf.a φ A : 0
4 pserf.r R = sup r | seq 0 + G r dom * <
5 psercn.s S = abs -1 0 R
6 psercn.m M = if R a + R 2 a + 1
7 pserdv.b B = 0 ball abs a + M 2
8 dvfcn F : dom F
9 ssidd φ
10 1 2 3 4 5 6 psercn φ F : S cn
11 cncff F : S cn F : S
12 10 11 syl φ F : S
13 cnvimass abs -1 0 R dom abs
14 absf abs :
15 14 fdmi dom abs =
16 13 15 sseqtri abs -1 0 R
17 5 16 eqsstri S
18 17 a1i φ S
19 9 12 18 dvbss φ dom F S
20 ssidd φ a S
21 12 adantr φ a S F : S
22 17 a1i φ a S S
23 cnxmet abs ∞Met
24 0cnd φ a S 0
25 18 sselda φ a S a
26 25 abscld φ a S a
27 1 2 3 4 5 6 psercnlem1 φ a S M + a < M M < R
28 27 simp1d φ a S M +
29 28 rpred φ a S M
30 26 29 readdcld φ a S a + M
31 0red φ a S 0
32 25 absge0d φ a S 0 a
33 26 28 ltaddrpd φ a S a < a + M
34 31 26 30 32 33 lelttrd φ a S 0 < a + M
35 30 34 elrpd φ a S a + M +
36 35 rphalfcld φ a S a + M 2 +
37 36 rpxrd φ a S a + M 2 *
38 blssm abs ∞Met 0 a + M 2 * 0 ball abs a + M 2
39 23 24 37 38 mp3an2i φ a S 0 ball abs a + M 2
40 7 39 eqsstrid φ a S B
41 eqid TopOpen fld = TopOpen fld
42 41 cnfldtopon TopOpen fld TopOn
43 42 toponrestid TopOpen fld = TopOpen fld 𝑡
44 41 43 dvres F : S S B D F B = F int TopOpen fld B
45 20 21 22 40 44 syl22anc φ a S D F B = F int TopOpen fld B
46 resss F int TopOpen fld B D F
47 45 46 eqsstrdi φ a S D F B D F
48 dmss D F B D F dom F B dom F
49 47 48 syl φ a S dom F B dom F
50 1 2 3 4 5 6 pserdvlem1 φ a S a + M 2 + a < a + M 2 a + M 2 < R
51 1 2 3 4 5 50 psercnlem2 φ a S a 0 ball abs a + M 2 0 ball abs a + M 2 abs -1 0 a + M 2 abs -1 0 a + M 2 S
52 51 simp1d φ a S a 0 ball abs a + M 2
53 52 7 eleqtrrdi φ a S a B
54 1 2 3 4 5 6 7 pserdvlem2 φ a S D F B = y B k 0 k + 1 A k + 1 y k
55 54 dmeqd φ a S dom F B = dom y B k 0 k + 1 A k + 1 y k
56 dmmptg y B k 0 k + 1 A k + 1 y k V dom y B k 0 k + 1 A k + 1 y k = B
57 sumex k 0 k + 1 A k + 1 y k V
58 57 a1i y B k 0 k + 1 A k + 1 y k V
59 56 58 mprg dom y B k 0 k + 1 A k + 1 y k = B
60 55 59 eqtrdi φ a S dom F B = B
61 53 60 eleqtrrd φ a S a dom F B
62 49 61 sseldd φ a S a dom F
63 19 62 eqelssd φ dom F = S
64 63 feq2d φ F : dom F F : S
65 8 64 mpbii φ F : S
66 65 feqmptd φ D F = a S F a
67 ffun F : dom F Fun F
68 8 67 mp1i φ a S Fun F
69 funssfv Fun F D F B D F a dom F B F a = F B a
70 68 47 61 69 syl3anc φ a S F a = F B a
71 54 fveq1d φ a S F B a = y B k 0 k + 1 A k + 1 y k a
72 oveq1 y = a y k = a k
73 72 oveq2d y = a k + 1 A k + 1 y k = k + 1 A k + 1 a k
74 73 sumeq2sdv y = a k 0 k + 1 A k + 1 y k = k 0 k + 1 A k + 1 a k
75 eqid y B k 0 k + 1 A k + 1 y k = y B k 0 k + 1 A k + 1 y k
76 sumex k 0 k + 1 A k + 1 a k V
77 74 75 76 fvmpt a B y B k 0 k + 1 A k + 1 y k a = k 0 k + 1 A k + 1 a k
78 53 77 syl φ a S y B k 0 k + 1 A k + 1 y k a = k 0 k + 1 A k + 1 a k
79 70 71 78 3eqtrd φ a S F a = k 0 k + 1 A k + 1 a k
80 79 mpteq2dva φ a S F a = a S k 0 k + 1 A k + 1 a k
81 66 80 eqtrd φ D F = a S k 0 k + 1 A k + 1 a k
82 oveq1 a = y a k = y k
83 82 oveq2d a = y k + 1 A k + 1 a k = k + 1 A k + 1 y k
84 83 sumeq2sdv a = y k 0 k + 1 A k + 1 a k = k 0 k + 1 A k + 1 y k
85 84 cbvmptv a S k 0 k + 1 A k + 1 a k = y S k 0 k + 1 A k + 1 y k
86 81 85 eqtrdi φ D F = y S k 0 k + 1 A k + 1 y k