# Metamath Proof Explorer

## Theorem taylpval

Description: Value of the Taylor polynomial. (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}$
taylpval.x ${⊢}{\phi }\to {X}\in ℂ$
Assertion taylpval ${⊢}{\phi }\to {T}\left({X}\right)=\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}}$

### 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 taylpval.x ${⊢}{\phi }\to {X}\in ℂ$
8 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)$
9 simplr ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {x}={X}$
10 9 oveq1d ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {x}-{B}={X}-{B}$
11 10 oveq1d ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {\left({x}-{B}\right)}^{{k}}={\left({X}-{B}\right)}^{{k}}$
12 11 oveq2d ${⊢}\left(\left({\phi }\wedge {x}={X}\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}}=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({X}-{B}\right)}^{{k}}$
13 12 sumeq2dv ${⊢}\left({\phi }\wedge {x}={X}\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}}=\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}}$
14 sumex ${⊢}\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 \mathrm{V}$
15 14 a1i ${⊢}{\phi }\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 \mathrm{V}$
16 8 13 7 15 fvmptd ${⊢}{\phi }\to {T}\left({X}\right)=\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}}$