# Metamath Proof Explorer

## Theorem taylfvallem

Description: Lemma for taylfval . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses taylfval.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
taylfval.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
taylfval.a ${⊢}{\phi }\to {A}\subseteq {S}$
taylfval.n ${⊢}{\phi }\to \left({N}\in {ℕ}_{0}\vee {N}=\mathrm{+\infty }\right)$
taylfval.b ${⊢}\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)$
Assertion taylfvallem ${⊢}\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)\subseteq ℂ$

### Proof

Step Hyp Ref Expression
1 taylfval.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 taylfval.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
3 taylfval.a ${⊢}{\phi }\to {A}\subseteq {S}$
4 taylfval.n ${⊢}{\phi }\to \left({N}\in {ℕ}_{0}\vee {N}=\mathrm{+\infty }\right)$
5 taylfval.b ${⊢}\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)$
6 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
7 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
8 ringcmn ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
9 7 8 mp1i ${⊢}\left({\phi }\wedge {X}\in ℂ\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
10 cnfldtps ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}$
11 10 a1i ${⊢}\left({\phi }\wedge {X}\in ℂ\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}$
12 ovex ${⊢}\left[0,{N}\right]\in \mathrm{V}$
13 12 inex1 ${⊢}\left[0,{N}\right]\cap ℤ\in \mathrm{V}$
14 13 a1i ${⊢}\left({\phi }\wedge {X}\in ℂ\right)\to \left[0,{N}\right]\cap ℤ\in \mathrm{V}$
15 1 2 3 4 5 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 ℂ$
16 15 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 ℤ⟶ℂ$
17 6 9 11 14 16 tsmscl ${⊢}\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)\subseteq ℂ$