# 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 ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
taylpfval.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
taylpfval.a ${⊢}{\phi }\to {A}\subseteq {S}$
taylpfval.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
taylpfval.b ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
taylpfval.t ${⊢}{T}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
Assertion taylpf ${⊢}{\phi }\to {T}:ℂ⟶ℂ$

### Proof

Step Hyp Ref Expression
1 taylpfval.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 taylpfval.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
3 taylpfval.a ${⊢}{\phi }\to {A}\subseteq {S}$
4 taylpfval.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
5 taylpfval.b ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
6 taylpfval.t ${⊢}{T}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
7 1 2 3 4 5 6 taylpfval ${⊢}{\phi }\to {T}=\left({x}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)$
8 fzfid ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left(0\dots {N}\right)\in \mathrm{Fin}$
9 1 2 3 4 5 taylplem2 ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\in ℂ$
10 8 9 fsumcl ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\in ℂ$
11 7 10 fmpt3d ${⊢}{\phi }\to {T}:ℂ⟶ℂ$