Theorem taylpf

Description: The Taylor polynomial is a function on the complex numbers (even if the base set of the original function is the reals). (Contributed by Mario Carneiro, 31-Dec-2016)

	Ref	Expression
Hypotheses	taylpfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	taylpfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	taylpfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
	taylpfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	taylpfval.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
	taylpfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
Assertion	taylpf	⊢ ( 𝜑 → 𝑇 : ℂ ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		taylpfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		taylpfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		taylpfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		taylpfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		taylpfval.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
6		taylpfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
7	1 2 3 4 5 6	taylpfval	⊢ ( 𝜑 → 𝑇 = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) )
8		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 0 ... 𝑁 ) ∈ Fin )
9	1 2 3 4 5	taylplem2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )
10	8 9	fsumcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )
11	7 10	fmpt3d	⊢ ( 𝜑 → 𝑇 : ℂ ⟶ ℂ )