# Metamath Proof Explorer

## Theorem tayl0

Description: The Taylor series is always defined at the basepoint, with value equal to the value 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 tayl0 ${⊢}{\phi }\to \left({B}\in \mathrm{dom}{T}\wedge {T}\left({B}\right)={F}\left({B}\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 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
8 1 7 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
9 3 8 sstrd ${⊢}{\phi }\to {A}\subseteq ℂ$
10 fveq2 ${⊢}{k}=0\to \left({S}{D}^{n}{F}\right)\left({k}\right)=\left({S}{D}^{n}{F}\right)\left(0\right)$
11 10 dmeqd ${⊢}{k}=0\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left(0\right)$
12 11 eleq2d ${⊢}{k}=0\to \left({B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)↔{B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left(0\right)\right)$
13 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)$
14 elxnn0 ${⊢}{N}\in {ℕ}_{0}^{*}↔\left({N}\in {ℕ}_{0}\vee {N}=\mathrm{+\infty }\right)$
15 0xr ${⊢}0\in {ℝ}^{*}$
16 15 a1i ${⊢}{N}\in {ℕ}_{0}^{*}\to 0\in {ℝ}^{*}$
17 xnn0xr ${⊢}{N}\in {ℕ}_{0}^{*}\to {N}\in {ℝ}^{*}$
18 xnn0ge0 ${⊢}{N}\in {ℕ}_{0}^{*}\to 0\le {N}$
19 lbicc2 ${⊢}\left(0\in {ℝ}^{*}\wedge {N}\in {ℝ}^{*}\wedge 0\le {N}\right)\to 0\in \left[0,{N}\right]$
20 16 17 18 19 syl3anc ${⊢}{N}\in {ℕ}_{0}^{*}\to 0\in \left[0,{N}\right]$
21 14 20 sylbir ${⊢}\left({N}\in {ℕ}_{0}\vee {N}=\mathrm{+\infty }\right)\to 0\in \left[0,{N}\right]$
22 4 21 syl ${⊢}{\phi }\to 0\in \left[0,{N}\right]$
23 0zd ${⊢}{\phi }\to 0\in ℤ$
24 22 23 elind ${⊢}{\phi }\to 0\in \left(\left[0,{N}\right]\cap ℤ\right)$
25 12 13 24 rspcdva ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left(0\right)$
26 cnex ${⊢}ℂ\in \mathrm{V}$
27 26 a1i ${⊢}{\phi }\to ℂ\in \mathrm{V}$
28 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)$
29 27 1 2 3 28 syl22anc ${⊢}{\phi }\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
30 dvn0 ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to \left({S}{D}^{n}{F}\right)\left(0\right)={F}$
31 8 29 30 syl2anc ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left(0\right)={F}$
32 31 dmeqd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left(0\right)=\mathrm{dom}{F}$
33 2 fdmd ${⊢}{\phi }\to \mathrm{dom}{F}={A}$
34 32 33 eqtrd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left(0\right)={A}$
35 25 34 eleqtrd ${⊢}{\phi }\to {B}\in {A}$
36 9 35 sseldd ${⊢}{\phi }\to {B}\in ℂ$
37 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
38 cnfld0 ${⊢}0={0}_{{ℂ}_{\mathrm{fld}}}$
39 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
40 ringmnd ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$
41 39 40 mp1i ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$
42 ovex ${⊢}\left[0,{N}\right]\in \mathrm{V}$
43 42 inex1 ${⊢}\left[0,{N}\right]\cap ℤ\in \mathrm{V}$
44 43 a1i ${⊢}{\phi }\to \left[0,{N}\right]\cap ℤ\in \mathrm{V}$
45 1 adantr ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {S}\in \left\{ℝ,ℂ\right\}$
46 29 adantr ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
47 simpr ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}\in \left(\left[0,{N}\right]\cap ℤ\right)$
48 47 elin2d ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}\in ℤ$
49 47 elin1d ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}\in \left[0,{N}\right]$
50 nn0re ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℝ$
51 50 rexrd ${⊢}{N}\in {ℕ}_{0}\to {N}\in {ℝ}^{*}$
52 id ${⊢}{N}=\mathrm{+\infty }\to {N}=\mathrm{+\infty }$
53 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
54 52 53 eqeltrdi ${⊢}{N}=\mathrm{+\infty }\to {N}\in {ℝ}^{*}$
55 51 54 jaoi ${⊢}\left({N}\in {ℕ}_{0}\vee {N}=\mathrm{+\infty }\right)\to {N}\in {ℝ}^{*}$
56 4 55 syl ${⊢}{\phi }\to {N}\in {ℝ}^{*}$
57 56 adantr ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {N}\in {ℝ}^{*}$
58 elicc1 ${⊢}\left(0\in {ℝ}^{*}\wedge {N}\in {ℝ}^{*}\right)\to \left({k}\in \left[0,{N}\right]↔\left({k}\in {ℝ}^{*}\wedge 0\le {k}\wedge {k}\le {N}\right)\right)$
59 15 57 58 sylancr ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to \left({k}\in \left[0,{N}\right]↔\left({k}\in {ℝ}^{*}\wedge 0\le {k}\wedge {k}\le {N}\right)\right)$
60 49 59 mpbid ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to \left({k}\in {ℝ}^{*}\wedge 0\le {k}\wedge {k}\le {N}\right)$
61 60 simp2d ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to 0\le {k}$
62 elnn0z ${⊢}{k}\in {ℕ}_{0}↔\left({k}\in ℤ\wedge 0\le {k}\right)$
63 48 61 62 sylanbrc ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}\in {ℕ}_{0}$
64 dvnf ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟶ℂ$
65 45 46 63 64 syl3anc ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟶ℂ$
66 65 5 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)\in ℂ$
67 63 faccld ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}!\in ℕ$
68 67 nncnd ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}!\in ℂ$
69 67 nnne0d ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}!\ne 0$
70 66 68 69 divcld ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\in ℂ$
71 0cnd ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to 0\in ℂ$
72 71 63 expcld ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {0}^{{k}}\in ℂ$
73 70 72 mulcld ${⊢}\left({\phi }\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){0}^{{k}}\in ℂ$
74 73 fmpttd ${⊢}{\phi }\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){0}^{{k}}\right):\left[0,{N}\right]\cap ℤ⟶ℂ$
75 eldifi ${⊢}{k}\in \left(\left(\left[0,{N}\right]\cap ℤ\right)\setminus \left\{0\right\}\right)\to {k}\in \left(\left[0,{N}\right]\cap ℤ\right)$
76 75 63 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left(\left(\left[0,{N}\right]\cap ℤ\right)\setminus \left\{0\right\}\right)\right)\to {k}\in {ℕ}_{0}$
77 eldifsni ${⊢}{k}\in \left(\left(\left[0,{N}\right]\cap ℤ\right)\setminus \left\{0\right\}\right)\to {k}\ne 0$
78 77 adantl ${⊢}\left({\phi }\wedge {k}\in \left(\left(\left[0,{N}\right]\cap ℤ\right)\setminus \left\{0\right\}\right)\right)\to {k}\ne 0$
79 elnnne0 ${⊢}{k}\in ℕ↔\left({k}\in {ℕ}_{0}\wedge {k}\ne 0\right)$
80 76 78 79 sylanbrc ${⊢}\left({\phi }\wedge {k}\in \left(\left(\left[0,{N}\right]\cap ℤ\right)\setminus \left\{0\right\}\right)\right)\to {k}\in ℕ$
81 80 0expd ${⊢}\left({\phi }\wedge {k}\in \left(\left(\left[0,{N}\right]\cap ℤ\right)\setminus \left\{0\right\}\right)\right)\to {0}^{{k}}=0$
82 81 oveq2d ${⊢}\left({\phi }\wedge {k}\in \left(\left(\left[0,{N}\right]\cap ℤ\right)\setminus \left\{0\right\}\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){0}^{{k}}=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)\cdot 0$
83 70 mul01d ${⊢}\left({\phi }\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)\cdot 0=0$
84 75 83 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left(\left(\left[0,{N}\right]\cap ℤ\right)\setminus \left\{0\right\}\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)\cdot 0=0$
85 82 84 eqtrd ${⊢}\left({\phi }\wedge {k}\in \left(\left(\left[0,{N}\right]\cap ℤ\right)\setminus \left\{0\right\}\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){0}^{{k}}=0$
86 zex ${⊢}ℤ\in \mathrm{V}$
87 86 inex2 ${⊢}\left[0,{N}\right]\cap ℤ\in \mathrm{V}$
88 87 a1i ${⊢}{\phi }\to \left[0,{N}\right]\cap ℤ\in \mathrm{V}$
89 85 88 suppss2 ${⊢}{\phi }\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){0}^{{k}}\right)\mathrm{supp}0\subseteq \left\{0\right\}$
90 37 38 41 44 24 74 89 gsumpt ${⊢}{\phi }\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){0}^{{k}}=\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){0}^{{k}}\right)\left(0\right)$
91 10 fveq1d ${⊢}{k}=0\to \left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)$
92 fveq2 ${⊢}{k}=0\to {k}!=0!$
93 fac0 ${⊢}0!=1$
94 92 93 syl6eq ${⊢}{k}=0\to {k}!=1$
95 91 94 oveq12d ${⊢}{k}=0\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}=\frac{\left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)}{1}$
96 oveq2 ${⊢}{k}=0\to {0}^{{k}}={0}^{0}$
97 0exp0e1 ${⊢}{0}^{0}=1$
98 96 97 syl6eq ${⊢}{k}=0\to {0}^{{k}}=1$
99 95 98 oveq12d ${⊢}{k}=0\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){0}^{{k}}=\left(\frac{\left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)}{1}\right)\cdot 1$
100 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){0}^{{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){0}^{{k}}\right)$
101 ovex ${⊢}\left(\frac{\left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)}{1}\right)\cdot 1\in \mathrm{V}$
102 99 100 101 fvmpt ${⊢}0\in \left(\left[0,{N}\right]\cap ℤ\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){0}^{{k}}\right)\left(0\right)=\left(\frac{\left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)}{1}\right)\cdot 1$
103 24 102 syl ${⊢}{\phi }\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){0}^{{k}}\right)\left(0\right)=\left(\frac{\left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)}{1}\right)\cdot 1$
104 31 fveq1d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)={F}\left({B}\right)$
105 104 oveq1d ${⊢}{\phi }\to \frac{\left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)}{1}=\frac{{F}\left({B}\right)}{1}$
106 2 35 ffvelrnd ${⊢}{\phi }\to {F}\left({B}\right)\in ℂ$
107 106 div1d ${⊢}{\phi }\to \frac{{F}\left({B}\right)}{1}={F}\left({B}\right)$
108 105 107 eqtrd ${⊢}{\phi }\to \frac{\left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)}{1}={F}\left({B}\right)$
109 108 oveq1d ${⊢}{\phi }\to \left(\frac{\left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)}{1}\right)\cdot 1={F}\left({B}\right)\cdot 1$
110 106 mulid1d ${⊢}{\phi }\to {F}\left({B}\right)\cdot 1={F}\left({B}\right)$
111 109 110 eqtrd ${⊢}{\phi }\to \left(\frac{\left({S}{D}^{n}{F}\right)\left(0\right)\left({B}\right)}{1}\right)\cdot 1={F}\left({B}\right)$
112 90 103 111 3eqtrd ${⊢}{\phi }\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){0}^{{k}}={F}\left({B}\right)$
113 ringcmn ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
114 39 113 mp1i ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
115 cnfldtps ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}$
116 115 a1i ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}$
117 mptexg ${⊢}\left[0,{N}\right]\cap ℤ\in \mathrm{V}\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){0}^{{k}}\right)\in \mathrm{V}$
118 87 117 mp1i ${⊢}{\phi }\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){0}^{{k}}\right)\in \mathrm{V}$
119 funmpt ${⊢}\mathrm{Fun}\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){0}^{{k}}\right)$
120 119 a1i ${⊢}{\phi }\to \mathrm{Fun}\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){0}^{{k}}\right)$
121 c0ex ${⊢}0\in \mathrm{V}$
122 121 a1i ${⊢}{\phi }\to 0\in \mathrm{V}$
123 snfi ${⊢}\left\{0\right\}\in \mathrm{Fin}$
124 123 a1i ${⊢}{\phi }\to \left\{0\right\}\in \mathrm{Fin}$
125 suppssfifsupp ${⊢}\left(\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){0}^{{k}}\right)\in \mathrm{V}\wedge \mathrm{Fun}\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){0}^{{k}}\right)\wedge 0\in \mathrm{V}\right)\wedge \left(\left\{0\right\}\in \mathrm{Fin}\wedge \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){0}^{{k}}\right)\mathrm{supp}0\subseteq \left\{0\right\}\right)\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){0}^{{k}}\right)\right)$
126 118 120 122 124 89 125 syl32anc ${⊢}{\phi }\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){0}^{{k}}\right)\right)$
127 37 38 114 116 44 74 126 tsmsid ${⊢}{\phi }\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){0}^{{k}}\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){0}^{{k}}\right)\right)$
128 112 127 eqeltrrd ${⊢}{\phi }\to {F}\left({B}\right)\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){0}^{{k}}\right)\right)$
129 36 subidd ${⊢}{\phi }\to {B}-{B}=0$
130 129 oveq1d ${⊢}{\phi }\to {\left({B}-{B}\right)}^{{k}}={0}^{{k}}$
131 130 oveq2d ${⊢}{\phi }\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({B}-{B}\right)}^{{k}}=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){0}^{{k}}$
132 131 mpteq2dv ${⊢}{\phi }\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({B}-{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){0}^{{k}}\right)$
133 132 oveq2d ${⊢}{\phi }\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({B}-{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){0}^{{k}}\right)$
134 128 133 eleqtrrd ${⊢}{\phi }\to {F}\left({B}\right)\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({B}-{B}\right)}^{{k}}\right)\right)$
135 1 2 3 4 5 6 eltayl ${⊢}{\phi }\to \left({B}{T}{F}\left({B}\right)↔\left({B}\in ℂ\wedge {F}\left({B}\right)\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({B}-{B}\right)}^{{k}}\right)\right)\right)\right)$
136 36 134 135 mpbir2and ${⊢}{\phi }\to {B}{T}{F}\left({B}\right)$
137 1 2 3 4 5 6 taylf ${⊢}{\phi }\to {T}:\mathrm{dom}{T}⟶ℂ$
138 ffun ${⊢}{T}:\mathrm{dom}{T}⟶ℂ\to \mathrm{Fun}{T}$
139 funbrfv2b ${⊢}\mathrm{Fun}{T}\to \left({B}{T}{F}\left({B}\right)↔\left({B}\in \mathrm{dom}{T}\wedge {T}\left({B}\right)={F}\left({B}\right)\right)\right)$
140 137 138 139 3syl ${⊢}{\phi }\to \left({B}{T}{F}\left({B}\right)↔\left({B}\in \mathrm{dom}{T}\wedge {T}\left({B}\right)={F}\left({B}\right)\right)\right)$
141 136 140 mpbid ${⊢}{\phi }\to \left({B}\in \mathrm{dom}{T}\wedge {T}\left({B}\right)={F}\left({B}\right)\right)$