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		ffvelcdm	⊢ ( ( 𝐴 : ℕ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 ) ) ) ) )