This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
pserf.f ⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
pserf.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
pserf.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
psercn.s ⊢ 𝑆 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
psercn.m ⊢ 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) )
pserdv.b ⊢ 𝐵 = ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) )
Assertion pserdv ( 𝜑 → ( ℂ D 𝐹 ) = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 pserf.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2 pserf.f ⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
3 pserf.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
4 pserf.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
5 psercn.s ⊢ 𝑆 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
6 psercn.m ⊢ 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) )
7 pserdv.b ⊢ 𝐵 = ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) )
8 dvfcn ⊢ ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ
9 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
10 1 2 3 4 5 6 psercn ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 –cn→ ℂ ) )
11 cncff ⊢ ( 𝐹 ∈ ( 𝑆 –cn→ ℂ ) → 𝐹 : 𝑆 ⟶ ℂ )
12 10 11 syl ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )
13 cnvimass ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ dom abs
14 absf ⊢ abs : ℂ ⟶ ℝ
15 14 fdmi ⊢ dom abs = ℂ
16 13 15 sseqtri ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ ℂ
17 5 16 eqsstri ⊢ 𝑆 ⊆ ℂ
18 17 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
19 9 12 18 dvbss ⊢ ( 𝜑 → dom ( ℂ D 𝐹 ) ⊆ 𝑆 )
20 ssidd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ℂ ⊆ ℂ )
21 12 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐹 : 𝑆 ⟶ ℂ )
22 17 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑆 ⊆ ℂ )
23 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
24 0cnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ∈ ℂ )
25 18 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ℂ )
26 25 abscld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) ∈ ℝ )
27 1 2 3 4 5 6 psercnlem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑀 ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < 𝑀 ∧ 𝑀 < 𝑅 ) )
28 27 simp1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ+ )
29 28 rpred ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
30 26 29 readdcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) + 𝑀 ) ∈ ℝ )
31 0red ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ∈ ℝ )
32 25 absge0d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ≤ ( abs ‘ 𝑎 ) )
33 26 28 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 𝑀 ) )
34 31 26 30 32 33 lelttrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 < ( ( abs ‘ 𝑎 ) + 𝑀 ) )
35 30 34 elrpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) + 𝑀 ) ∈ ℝ+ )
36 35 rphalfcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ+ )
37 36 rpxrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ* )
38 blssm ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ⊆ ℂ )
39 23 24 37 38 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ⊆ ℂ )
40 7 39 eqsstrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐵 ⊆ ℂ )
41 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
42 41 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
43 42 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
44 41 43 dvres ⊢ ( ( ( ℂ ⊆ ℂ ∧ 𝐹 : 𝑆 ⟶ ℂ ) ∧ ( 𝑆 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ) → ( ℂ D ( 𝐹 ↾ 𝐵 ) ) = ( ( ℂ D 𝐹 ) ↾ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) ) )
45 20 21 22 40 44 syl22anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ℂ D ( 𝐹 ↾ 𝐵 ) ) = ( ( ℂ D 𝐹 ) ↾ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) ) )
46 resss ⊢ ( ( ℂ D 𝐹 ) ↾ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) ) ⊆ ( ℂ D 𝐹 )
47 45 46 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ℂ D ( 𝐹 ↾ 𝐵 ) ) ⊆ ( ℂ D 𝐹 ) )
48 dmss ⊢ ( ( ℂ D ( 𝐹 ↾ 𝐵 ) ) ⊆ ( ℂ D 𝐹 ) → dom ( ℂ D ( 𝐹 ↾ 𝐵 ) ) ⊆ dom ( ℂ D 𝐹 ) )
49 47 48 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → dom ( ℂ D ( 𝐹 ↾ 𝐵 ) ) ⊆ dom ( ℂ D 𝐹 ) )
50 1 2 3 4 5 6 pserdvlem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∧ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑅 ) )
51 1 2 3 4 5 50 psercnlem2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ⊆ ( ◡ abs “ ( 0 [,] ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ) ∧ ( ◡ abs “ ( 0 [,] ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ) ⊆ 𝑆 ) )
52 51 simp1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) )
53 52 7 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝐵 )
54 1 2 3 4 5 6 7 pserdvlem2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ℂ D ( 𝐹 ↾ 𝐵 ) ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
55 54 dmeqd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → dom ( ℂ D ( 𝐹 ↾ 𝐵 ) ) = dom ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
56 dmmptg ⊢ ( ∀ 𝑦 ∈ 𝐵 Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ∈ V → dom ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) = 𝐵 )
57 sumex ⊢ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ∈ V
58 57 a1i ⊢ ( 𝑦 ∈ 𝐵 → Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ∈ V )
59 56 58 mprg ⊢ dom ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) = 𝐵
60 55 59 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → dom ( ℂ D ( 𝐹 ↾ 𝐵 ) ) = 𝐵 )
61 53 60 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ dom ( ℂ D ( 𝐹 ↾ 𝐵 ) ) )
62 49 61 sseldd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ dom ( ℂ D 𝐹 ) )
63 19 62 eqelssd ⊢ ( 𝜑 → dom ( ℂ D 𝐹 ) = 𝑆 )
64 63 feq2d ⊢ ( 𝜑 → ( ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ ↔ ( ℂ D 𝐹 ) : 𝑆 ⟶ ℂ ) )
65 8 64 mpbii ⊢ ( 𝜑 → ( ℂ D 𝐹 ) : 𝑆 ⟶ ℂ )
66 65 feqmptd ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( 𝑎 ∈ 𝑆 ↦ ( ( ℂ D 𝐹 ) ‘ 𝑎 ) ) )
67 ffun ⊢ ( ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ → Fun ( ℂ D 𝐹 ) )
68 8 67 mp1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → Fun ( ℂ D 𝐹 ) )
69 funssfv ⊢ ( ( Fun ( ℂ D 𝐹 ) ∧ ( ℂ D ( 𝐹 ↾ 𝐵 ) ) ⊆ ( ℂ D 𝐹 ) ∧ 𝑎 ∈ dom ( ℂ D ( 𝐹 ↾ 𝐵 ) ) ) → ( ( ℂ D 𝐹 ) ‘ 𝑎 ) = ( ( ℂ D ( 𝐹 ↾ 𝐵 ) ) ‘ 𝑎 ) )
70 68 47 61 69 syl3anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ℂ D 𝐹 ) ‘ 𝑎 ) = ( ( ℂ D ( 𝐹 ↾ 𝐵 ) ) ‘ 𝑎 ) )
71 54 fveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ℂ D ( 𝐹 ↾ 𝐵 ) ) ‘ 𝑎 ) = ( ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝑎 ) )
72 oveq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 ↑ 𝑘 ) = ( 𝑎 ↑ 𝑘 ) )
73 72 oveq2d ⊢ ( 𝑦 = 𝑎 → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) )
74 73 sumeq2sdv ⊢ ( 𝑦 = 𝑎 → Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) )
75 eqid ⊢ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
76 sumex ⊢ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) ∈ V
77 74 75 76 fvmpt ⊢ ( 𝑎 ∈ 𝐵 → ( ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝑎 ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) )
78 53 77 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝑎 ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) )
79 70 71 78 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ℂ D 𝐹 ) ‘ 𝑎 ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) )
80 79 mpteq2dva ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑆 ↦ ( ( ℂ D 𝐹 ) ‘ 𝑎 ) ) = ( 𝑎 ∈ 𝑆 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) ) )
81 66 80 eqtrd ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( 𝑎 ∈ 𝑆 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) ) )
82 oveq1 ⊢ ( 𝑎 = 𝑦 → ( 𝑎 ↑ 𝑘 ) = ( 𝑦 ↑ 𝑘 ) )
83 82 oveq2d ⊢ ( 𝑎 = 𝑦 → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
84 83 sumeq2sdv ⊢ ( 𝑎 = 𝑦 → Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
85 84 cbvmptv ⊢ ( 𝑎 ∈ 𝑆 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑎 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
86 81 85 eqtrdi ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )