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 ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ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 pserdv2 ( 𝜑 → ( ℂ D 𝐹 ) = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑘 ∈ ℕ ( ( 𝑘 · ( 𝐴 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 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 1 2 3 4 5 6 7 pserdv ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑚 ∈ ℕ0 ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑦 ↑ 𝑚 ) ) ) )
9 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
10 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
11 1e0p1 ⊢ 1 = ( 0 + 1 )
12 11 fveq2i ⊢ ( ℤ≥ ‘ 1 ) = ( ℤ≥ ‘ ( 0 + 1 ) )
13 10 12 eqtri ⊢ ℕ = ( ℤ≥ ‘ ( 0 + 1 ) )
14 id ⊢ ( 𝑘 = ( 1 + 𝑚 ) → 𝑘 = ( 1 + 𝑚 ) )
15 fveq2 ⊢ ( 𝑘 = ( 1 + 𝑚 ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ ( 1 + 𝑚 ) ) )
16 14 15 oveq12d ⊢ ( 𝑘 = ( 1 + 𝑚 ) → ( 𝑘 · ( 𝐴 ‘ 𝑘 ) ) = ( ( 1 + 𝑚 ) · ( 𝐴 ‘ ( 1 + 𝑚 ) ) ) )
17 oveq1 ⊢ ( 𝑘 = ( 1 + 𝑚 ) → ( 𝑘 − 1 ) = ( ( 1 + 𝑚 ) − 1 ) )
18 17 oveq2d ⊢ ( 𝑘 = ( 1 + 𝑚 ) → ( 𝑦 ↑ ( 𝑘 − 1 ) ) = ( 𝑦 ↑ ( ( 1 + 𝑚 ) − 1 ) ) )
19 16 18 oveq12d ⊢ ( 𝑘 = ( 1 + 𝑚 ) → ( ( 𝑘 · ( 𝐴 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) = ( ( ( 1 + 𝑚 ) · ( 𝐴 ‘ ( 1 + 𝑚 ) ) ) · ( 𝑦 ↑ ( ( 1 + 𝑚 ) − 1 ) ) ) )
20 1zzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 1 ∈ ℤ )
21 0zd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 0 ∈ ℤ )
22 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
24 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
25 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
26 ffvelrn ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
27 24 25 26 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
28 23 27 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
29 cnvimass ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ dom abs
30 absf ⊢ abs : ℂ ⟶ ℝ
31 30 fdmi ⊢ dom abs = ℂ
32 29 31 sseqtri ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ ℂ
33 5 32 eqsstri ⊢ 𝑆 ⊆ ℂ
34 33 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
35 34 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ℂ )
36 nnm1nn0 ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 − 1 ) ∈ ℕ0 )
37 expcl ⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑘 − 1 ) ∈ ℕ0 ) → ( 𝑦 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
38 35 36 37 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑦 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
39 28 38 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 𝐴 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ∈ ℂ )
40 9 13 19 20 21 39 isumshft ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → Σ 𝑘 ∈ ℕ ( ( 𝑘 · ( 𝐴 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) = Σ 𝑚 ∈ ℕ0 ( ( ( 1 + 𝑚 ) · ( 𝐴 ‘ ( 1 + 𝑚 ) ) ) · ( 𝑦 ↑ ( ( 1 + 𝑚 ) − 1 ) ) ) )
41 ax-1cn ⊢ 1 ∈ ℂ
42 nn0cn ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℂ )
43 42 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℂ )
44 addcom ⊢ ( ( 1 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 1 + 𝑚 ) = ( 𝑚 + 1 ) )
45 41 43 44 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( 1 + 𝑚 ) = ( 𝑚 + 1 ) )
46 45 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ‘ ( 1 + 𝑚 ) ) = ( 𝐴 ‘ ( 𝑚 + 1 ) ) )
47 45 46 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 1 + 𝑚 ) · ( 𝐴 ‘ ( 1 + 𝑚 ) ) ) = ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) )
48 pncan2 ⊢ ( ( 1 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 1 + 𝑚 ) − 1 ) = 𝑚 )
49 41 43 48 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 1 + 𝑚 ) − 1 ) = 𝑚 )
50 49 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑦 ↑ ( ( 1 + 𝑚 ) − 1 ) ) = ( 𝑦 ↑ 𝑚 ) )
51 47 50 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 1 + 𝑚 ) · ( 𝐴 ‘ ( 1 + 𝑚 ) ) ) · ( 𝑦 ↑ ( ( 1 + 𝑚 ) − 1 ) ) ) = ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑦 ↑ 𝑚 ) ) )
52 51 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → Σ 𝑚 ∈ ℕ0 ( ( ( 1 + 𝑚 ) · ( 𝐴 ‘ ( 1 + 𝑚 ) ) ) · ( 𝑦 ↑ ( ( 1 + 𝑚 ) − 1 ) ) ) = Σ 𝑚 ∈ ℕ0 ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑦 ↑ 𝑚 ) ) )
53 40 52 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → Σ 𝑚 ∈ ℕ0 ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑦 ↑ 𝑚 ) ) = Σ 𝑘 ∈ ℕ ( ( 𝑘 · ( 𝐴 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) )
54 53 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 ↦ Σ 𝑚 ∈ ℕ0 ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑦 ↑ 𝑚 ) ) ) = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑘 ∈ ℕ ( ( 𝑘 · ( 𝐴 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) )
55 8 54 eqtrd ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑘 ∈ ℕ ( ( 𝑘 · ( 𝐴 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) )