# Metamath Proof Explorer

## Theorem taylfval

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 .

This "extended" version of taylpfval additionally handles the case N = +oo , in which case this is not a polynomial but an infinite series, the Taylor series of the function. (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 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)$

### 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 df-tayl ${⊢}\mathrm{Tayl}=\left({s}\in \left\{ℝ,ℂ\right\},{f}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)⟼\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)⟼\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)\right)$
8 7 a1i ${⊢}{\phi }\to \mathrm{Tayl}=\left({s}\in \left\{ℝ,ℂ\right\},{f}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)⟼\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)⟼\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)\right)$
9 eqidd ${⊢}\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\right)\to {ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}={ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}$
10 oveq12 ${⊢}\left({s}={S}\wedge {f}={F}\right)\to {s}{D}^{n}{f}={S}{D}^{n}{F}$
11 10 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\right)\wedge {k}\in \left(\left[0,{n}\right]\cap ℤ\right)\right)\to {s}{D}^{n}{f}={S}{D}^{n}{F}$
12 11 fveq1d ${⊢}\left(\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\right)\wedge {k}\in \left(\left[0,{n}\right]\cap ℤ\right)\right)\to \left({s}{D}^{n}{f}\right)\left({k}\right)=\left({S}{D}^{n}{F}\right)\left({k}\right)$
13 12 dmeqd ${⊢}\left(\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\right)\wedge {k}\in \left(\left[0,{n}\right]\cap ℤ\right)\right)\to \mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
14 13 iineq2dv ${⊢}\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\right)\to \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)=\bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
15 12 fveq1d ${⊢}\left(\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\right)\wedge {k}\in \left(\left[0,{n}\right]\cap ℤ\right)\right)\to \left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)=\left({S}{D}^{n}{F}\right)\left({k}\right)\left({a}\right)$
16 15 oveq1d ${⊢}\left(\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\right)\wedge {k}\in \left(\left[0,{n}\right]\cap ℤ\right)\right)\to \frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}=\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({a}\right)}{{k}!}$
17 16 oveq1d ${⊢}\left(\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}$
18 17 mpteq2dva ${⊢}\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\right)\to \left({k}\in \left(\left[0,{n}\right]\cap ℤ\right)⟼\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)$
19 18 oveq2d ${⊢}\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\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({a}\right)}{{k}!}\right){\left({x}-{a}\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)$
20 19 xpeq2d ${⊢}\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)=\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)$
21 20 iuneq2d ${⊢}\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\right)\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)=\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)$
22 9 14 21 mpoeq123dv ${⊢}\left({\phi }\wedge \left({s}={S}\wedge {f}={F}\right)\right)\to \left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)⟼\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)=\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟼\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)$
23 simpr ${⊢}\left({\phi }\wedge {s}={S}\right)\to {s}={S}$
24 23 oveq2d ${⊢}\left({\phi }\wedge {s}={S}\right)\to ℂ{↑}_{𝑝𝑚}{s}=ℂ{↑}_{𝑝𝑚}{S}$
25 cnex ${⊢}ℂ\in \mathrm{V}$
26 25 a1i ${⊢}{\phi }\to ℂ\in \mathrm{V}$
27 elpm2r ${⊢}\left(\left(ℂ\in \mathrm{V}\wedge {S}\in \left\{ℝ,ℂ\right\}\right)\wedge \left({F}:{A}⟶ℂ\wedge {A}\subseteq {S}\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
28 26 1 2 3 27 syl22anc ${⊢}{\phi }\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
29 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
30 snex ${⊢}\left\{\mathrm{+\infty }\right\}\in \mathrm{V}$
31 29 30 unex ${⊢}{ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\in \mathrm{V}$
32 0xr ${⊢}0\in {ℝ}^{*}$
33 nn0ssre ${⊢}{ℕ}_{0}\subseteq ℝ$
34 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
35 33 34 sstri ${⊢}{ℕ}_{0}\subseteq {ℝ}^{*}$
36 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
37 snssi ${⊢}\mathrm{+\infty }\in {ℝ}^{*}\to \left\{\mathrm{+\infty }\right\}\subseteq {ℝ}^{*}$
38 36 37 ax-mp ${⊢}\left\{\mathrm{+\infty }\right\}\subseteq {ℝ}^{*}$
39 35 38 unssi ${⊢}{ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\subseteq {ℝ}^{*}$
40 39 sseli ${⊢}{n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)\to {n}\in {ℝ}^{*}$
41 elun ${⊢}{n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)↔\left({n}\in {ℕ}_{0}\vee {n}\in \left\{\mathrm{+\infty }\right\}\right)$
42 nn0ge0 ${⊢}{n}\in {ℕ}_{0}\to 0\le {n}$
43 0lepnf ${⊢}0\le \mathrm{+\infty }$
44 elsni ${⊢}{n}\in \left\{\mathrm{+\infty }\right\}\to {n}=\mathrm{+\infty }$
45 43 44 breqtrrid ${⊢}{n}\in \left\{\mathrm{+\infty }\right\}\to 0\le {n}$
46 42 45 jaoi ${⊢}\left({n}\in {ℕ}_{0}\vee {n}\in \left\{\mathrm{+\infty }\right\}\right)\to 0\le {n}$
47 41 46 sylbi ${⊢}{n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)\to 0\le {n}$
48 lbicc2 ${⊢}\left(0\in {ℝ}^{*}\wedge {n}\in {ℝ}^{*}\wedge 0\le {n}\right)\to 0\in \left[0,{n}\right]$
49 32 40 47 48 mp3an2i ${⊢}{n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)\to 0\in \left[0,{n}\right]$
50 0z ${⊢}0\in ℤ$
51 inelcm ${⊢}\left(0\in \left[0,{n}\right]\wedge 0\in ℤ\right)\to \left[0,{n}\right]\cap ℤ\ne \varnothing$
52 49 50 51 sylancl ${⊢}{n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)\to \left[0,{n}\right]\cap ℤ\ne \varnothing$
53 fvex ${⊢}\left({S}{D}^{n}{F}\right)\left({k}\right)\in \mathrm{V}$
54 53 dmex ${⊢}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\in \mathrm{V}$
55 54 rgenw ${⊢}\forall {k}\in \left(\left[0,{n}\right]\cap ℤ\right)\phantom{\rule{.4em}{0ex}}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\in \mathrm{V}$
56 iinexg ${⊢}\left(\left[0,{n}\right]\cap ℤ\ne \varnothing \wedge \forall {k}\in \left(\left[0,{n}\right]\cap ℤ\right)\phantom{\rule{.4em}{0ex}}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\in \mathrm{V}\right)\to \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\in \mathrm{V}$
57 52 55 56 sylancl ${⊢}{n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)\to \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\in \mathrm{V}$
58 57 rgen ${⊢}\forall {n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}\bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\in \mathrm{V}$
59 eqid ${⊢}\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟼\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)=\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟼\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)$
60 59 mpoexxg ${⊢}\left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\in \mathrm{V}\wedge \forall {n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}\bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\in \mathrm{V}\right)\to \left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟼\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)\in \mathrm{V}$
61 31 58 60 mp2an ${⊢}\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟼\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)\in \mathrm{V}$
62 61 a1i ${⊢}{\phi }\to \left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟼\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)\in \mathrm{V}$
63 8 22 24 1 28 62 ovmpodx ${⊢}{\phi }\to {S}\mathrm{Tayl}{F}=\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟼\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)$
64 simprl ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\to {n}={N}$
65 64 oveq2d ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\to \left[0,{n}\right]=\left[0,{N}\right]$
66 65 ineq1d ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\to \left[0,{n}\right]\cap ℤ=\left[0,{N}\right]\cap ℤ$
67 simprr ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\to {a}={B}$
68 67 fveq2d ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right)\left({a}\right)=\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)$
69 68 oveq1d ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({a}\right)}{{k}!}=\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}$
70 67 oveq2d ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\to {x}-{a}={x}-{B}$
71 70 oveq1d ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\to {\left({x}-{a}\right)}^{{k}}={\left({x}-{B}\right)}^{{k}}$
72 69 71 oveq12d ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}$
73 66 72 mpteq12dv ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\to \left({k}\in \left(\left[0,{n}\right]\cap ℤ\right)⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\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)$
74 73 oveq2d ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\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({a}\right)}{{k}!}\right){\left({x}-{a}\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)$
75 74 xpeq2d ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)=\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)$
76 75 iuneq2d ${⊢}\left({\phi }\wedge \left({n}={N}\wedge {a}={B}\right)\right)\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({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)=\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)$
77 simpr ${⊢}\left({\phi }\wedge {n}={N}\right)\to {n}={N}$
78 77 oveq2d ${⊢}\left({\phi }\wedge {n}={N}\right)\to \left[0,{n}\right]=\left[0,{N}\right]$
79 78 ineq1d ${⊢}\left({\phi }\wedge {n}={N}\right)\to \left[0,{n}\right]\cap ℤ=\left[0,{N}\right]\cap ℤ$
80 iineq1 ${⊢}\left[0,{n}\right]\cap ℤ=\left[0,{N}\right]\cap ℤ\to \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)=\bigcap _{{k}\in \left[0,{N}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
81 79 80 syl ${⊢}\left({\phi }\wedge {n}={N}\right)\to \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)=\bigcap _{{k}\in \left[0,{N}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
82 pnfex ${⊢}\mathrm{+\infty }\in \mathrm{V}$
83 82 elsn2 ${⊢}{N}\in \left\{\mathrm{+\infty }\right\}↔{N}=\mathrm{+\infty }$
84 83 orbi2i ${⊢}\left({N}\in {ℕ}_{0}\vee {N}\in \left\{\mathrm{+\infty }\right\}\right)↔\left({N}\in {ℕ}_{0}\vee {N}=\mathrm{+\infty }\right)$
85 4 84 sylibr ${⊢}{\phi }\to \left({N}\in {ℕ}_{0}\vee {N}\in \left\{\mathrm{+\infty }\right\}\right)$
86 elun ${⊢}{N}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)↔\left({N}\in {ℕ}_{0}\vee {N}\in \left\{\mathrm{+\infty }\right\}\right)$
87 85 86 sylibr ${⊢}{\phi }\to {N}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)$
88 5 ralrimiva ${⊢}{\phi }\to \forall {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
89 oveq2 ${⊢}{n}={N}\to \left[0,{n}\right]=\left[0,{N}\right]$
90 89 ineq1d ${⊢}{n}={N}\to \left[0,{n}\right]\cap ℤ=\left[0,{N}\right]\cap ℤ$
91 90 neeq1d ${⊢}{n}={N}\to \left(\left[0,{n}\right]\cap ℤ\ne \varnothing ↔\left[0,{N}\right]\cap ℤ\ne \varnothing \right)$
92 91 52 vtoclga ${⊢}{N}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)\to \left[0,{N}\right]\cap ℤ\ne \varnothing$
93 87 92 syl ${⊢}{\phi }\to \left[0,{N}\right]\cap ℤ\ne \varnothing$
94 r19.2z ${⊢}\left(\left[0,{N}\right]\cap ℤ\ne \varnothing \wedge \forall {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\right)\to \exists {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
95 93 88 94 syl2anc ${⊢}{\phi }\to \exists {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
96 elex ${⊢}{B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\to {B}\in \mathrm{V}$
97 96 rexlimivw ${⊢}\exists {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\to {B}\in \mathrm{V}$
98 eliin ${⊢}{B}\in \mathrm{V}\to \left({B}\in \bigcap _{{k}\in \left[0,{N}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)↔\forall {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\right)$
99 95 97 98 3syl ${⊢}{\phi }\to \left({B}\in \bigcap _{{k}\in \left[0,{N}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)↔\forall {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\right)$
100 88 99 mpbird ${⊢}{\phi }\to {B}\in \bigcap _{{k}\in \left[0,{N}\right]\cap ℤ}\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
101 snssi ${⊢}{x}\in ℂ\to \left\{{x}\right\}\subseteq ℂ$
102 1 2 3 4 5 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 ℂ$
103 xpss12 ${⊢}\left(\left\{{x}\right\}\subseteq ℂ\wedge {ℂ}_{\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 ℂ\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)\subseteq ℂ×ℂ$
104 101 102 103 syl2an2 ${⊢}\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)\subseteq ℂ×ℂ$
105 104 ralrimiva ${⊢}{\phi }\to \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\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)\subseteq ℂ×ℂ$
106 iunss ${⊢}\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)\subseteq ℂ×ℂ↔\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\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)\subseteq ℂ×ℂ$
107 105 106 sylibr ${⊢}{\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)\subseteq ℂ×ℂ$
108 25 25 xpex ${⊢}ℂ×ℂ\in \mathrm{V}$
109 108 ssex ${⊢}\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)\subseteq ℂ×ℂ\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)\in \mathrm{V}$
110 107 109 syl ${⊢}{\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)\in \mathrm{V}$
111 63 76 81 87 100 110 ovmpodx ${⊢}{\phi }\to {N}\left({S}\mathrm{Tayl}{F}\right){B}=\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)$
112 6 111 syl5eq ${⊢}{\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)$