# Metamath Proof Explorer

## Theorem eltayl

Description: Value of the Taylor series as a relation (elementhood in the domain here expresses that the series is convergent). (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)$
taylfval.t ${⊢}{T}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
Assertion eltayl ${⊢}{\phi }\to \left({X}{T}{Y}↔\left({X}\in ℂ\wedge {Y}\in \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)\right)$

### 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 taylfval.t ${⊢}{T}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
7 1 2 3 4 5 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)$
8 7 eleq2d ${⊢}{\phi }\to \left(⟨{X},{Y}⟩\in {T}↔⟨{X},{Y}⟩\in \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)\right)$
9 df-br ${⊢}{X}{T}{Y}↔⟨{X},{Y}⟩\in {T}$
10 9 bicomi ${⊢}⟨{X},{Y}⟩\in {T}↔{X}{T}{Y}$
11 oveq1 ${⊢}{x}={X}\to {x}-{B}={X}-{B}$
12 11 oveq1d ${⊢}{x}={X}\to {\left({x}-{B}\right)}^{{k}}={\left({X}-{B}\right)}^{{k}}$
13 12 oveq2d ${⊢}{x}={X}\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}}$
14 13 mpteq2dv ${⊢}{x}={X}\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({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)$
15 14 oveq2d ${⊢}{x}={X}\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)={ℂ}_{\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)$
16 15 opeliunxp2 ${⊢}⟨{X},{Y}⟩\in \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)↔\left({X}\in ℂ\wedge {Y}\in \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)$
17 8 10 16 3bitr3g ${⊢}{\phi }\to \left({X}{T}{Y}↔\left({X}\in ℂ\wedge {Y}\in \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)\right)$