# Metamath Proof Explorer

## Theorem taylpfval

Description: Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: S is the base set with respect to evaluate the derivatives (generally RR or CC ), F is the function we are approximating, at point B , to order N . The result is a polynomial function of x . (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 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)$

### 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 4 orcd ${⊢}{\phi }\to \left({N}\in {ℕ}_{0}\vee {N}=\mathrm{+\infty }\right)$
8 1 2 3 4 5 taylplem1 ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
9 1 2 3 7 8 6 taylfval ${⊢}{\phi }\to {T}=\bigcup _{{x}\in ℂ}\left(\left\{{x}\right\}×\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{N}\right]\cap ℤ\right)⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)\right)\right)$
10 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
11 cnfld0 ${⊢}0={0}_{{ℂ}_{\mathrm{fld}}}$
12 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
13 ringcmn ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
14 12 13 mp1i ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
15 cnfldtps ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}$
16 15 a1i ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}$
17 ovex ${⊢}\left[0,{N}\right]\in \mathrm{V}$
18 17 inex1 ${⊢}\left[0,{N}\right]\cap ℤ\in \mathrm{V}$
19 18 a1i ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left[0,{N}\right]\cap ℤ\in \mathrm{V}$
20 1 2 3 7 8 taylfvallem1 ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\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 ℂ$
21 20 fmpttd ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left({k}\in \left(\left[0,{N}\right]\cap ℤ\right)⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right):\left[0,{N}\right]\cap ℤ⟶ℂ$
22 eqid ${⊢}\left({k}\in \left(\left[0,{N}\right]\cap ℤ\right)⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)=\left({k}\in \left(\left[0,{N}\right]\cap ℤ\right)⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)$
23 0z ${⊢}0\in ℤ$
24 4 nn0zd ${⊢}{\phi }\to {N}\in ℤ$
25 fzval2 ${⊢}\left(0\in ℤ\wedge {N}\in ℤ\right)\to \left(0\dots {N}\right)=\left[0,{N}\right]\cap ℤ$
26 23 24 25 sylancr ${⊢}{\phi }\to \left(0\dots {N}\right)=\left[0,{N}\right]\cap ℤ$
27 26 adantr ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left(0\dots {N}\right)=\left[0,{N}\right]\cap ℤ$
28 fzfid ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left(0\dots {N}\right)\in \mathrm{Fin}$
29 27 28 eqeltrrd ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left[0,{N}\right]\cap ℤ\in \mathrm{Fin}$
30 ovexd ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\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 \mathrm{V}$
31 c0ex ${⊢}0\in \mathrm{V}$
32 31 a1i ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to 0\in \mathrm{V}$
33 22 29 30 32 fsuppmptdm ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {finSupp}_{0}\left(\left({k}\in \left(\left[0,{N}\right]\cap ℤ\right)⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)\right)$
34 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
35 34 cnfldhaus ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}$
36 35 a1i ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}$
37 10 11 14 16 19 21 33 34 36 haustsmsid ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{N}\right]\cap ℤ\right)⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)=\left\{\underset{{k}\in \left[0,{N}\right]\cap ℤ}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right\}$
38 29 20 gsumfsum ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \underset{{k}\in \left[0,{N}\right]\cap ℤ}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}=\sum _{{k}\in \left[0,{N}\right]\cap ℤ}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}$
39 27 sumeq1d ${⊢}\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}}=\sum _{{k}\in \left[0,{N}\right]\cap ℤ}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}$
40 38 39 eqtr4d ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \underset{{k}\in \left[0,{N}\right]\cap ℤ}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\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}}$
41 40 sneqd ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left\{\underset{{k}\in \left[0,{N}\right]\cap ℤ}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right\}=\left\{\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\}$
42 37 41 eqtrd ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{N}\right]\cap ℤ\right)⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)=\left\{\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\}$
43 42 xpeq2d ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left\{{x}\right\}×\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{N}\right]\cap ℤ\right)⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)\right)=\left\{{x}\right\}×\left\{\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\}$
44 43 iuneq2dv ${⊢}{\phi }\to \bigcup _{{x}\in ℂ}\left(\left\{{x}\right\}×\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{N}\right]\cap ℤ\right)⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)\right)\right)=\bigcup _{{x}\in ℂ}\left(\left\{{x}\right\}×\left\{\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\}\right)$
45 9 44 eqtrd ${⊢}{\phi }\to {T}=\bigcup _{{x}\in ℂ}\left(\left\{{x}\right\}×\left\{\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\}\right)$
46 dfmpt3 ${⊢}\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)=\bigcup _{{x}\in ℂ}\left(\left\{{x}\right\}×\left\{\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\}\right)$
47 45 46 eqtr4di ${⊢}{\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)$