Metamath Proof Explorer


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 ( 𝜑𝑇 : ℂ ⟶ ℂ )