# Metamath Proof Explorer

## Theorem taylply2

Description: The Taylor polynomial is a polynomial of degree (at most) N . This version of taylply shows that the coefficients of T are in a subring of the complex numbers. (Contributed by Mario Carneiro, 1-Jan-2017)

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}$
taylply2.1 ${⊢}{\phi }\to {D}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$
taylply2.2 ${⊢}{\phi }\to {B}\in {D}$
taylply2.3 ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\in {D}$
Assertion taylply2 ${⊢}{\phi }\to \left({T}\in \mathrm{Poly}\left({D}\right)\wedge \mathrm{deg}\left({T}\right)\le {N}\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 taylply2.1 ${⊢}{\phi }\to {D}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$
8 taylply2.2 ${⊢}{\phi }\to {B}\in {D}$
9 taylply2.3 ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\in {D}$
10 1 2 3 4 5 6 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)$
11 simpr ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {x}\in ℂ$
12 cnex ${⊢}ℂ\in \mathrm{V}$
13 12 a1i ${⊢}{\phi }\to ℂ\in \mathrm{V}$
14 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)$
15 13 1 2 3 14 syl22anc ${⊢}{\phi }\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
16 dvnbss ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq \mathrm{dom}{F}$
17 1 15 4 16 syl3anc ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq \mathrm{dom}{F}$
18 2 17 fssdmd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq {A}$
19 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
20 1 19 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
21 3 20 sstrd ${⊢}{\phi }\to {A}\subseteq ℂ$
22 18 21 sstrd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq ℂ$
23 22 5 sseldd ${⊢}{\phi }\to {B}\in ℂ$
24 23 adantr ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {B}\in ℂ$
25 11 24 subcld ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {x}-{B}\in ℂ$
26 df-idp ${⊢}{X}^{p}={\mathrm{I}↾}_{ℂ}$
27 mptresid ${⊢}{\mathrm{I}↾}_{ℂ}=\left({x}\in ℂ⟼{x}\right)$
28 26 27 eqtri ${⊢}{X}^{p}=\left({x}\in ℂ⟼{x}\right)$
29 28 a1i ${⊢}{\phi }\to {X}^{p}=\left({x}\in ℂ⟼{x}\right)$
30 fconstmpt ${⊢}ℂ×\left\{{B}\right\}=\left({x}\in ℂ⟼{B}\right)$
31 30 a1i ${⊢}{\phi }\to ℂ×\left\{{B}\right\}=\left({x}\in ℂ⟼{B}\right)$
32 13 11 24 29 31 offval2 ${⊢}{\phi }\to {X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)=\left({x}\in ℂ⟼{x}-{B}\right)$
33 eqidd ${⊢}{\phi }\to \left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)=\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)$
34 oveq1 ${⊢}{y}={x}-{B}\to {{y}}^{{k}}={\left({x}-{B}\right)}^{{k}}$
35 34 oveq2d ${⊢}{y}={x}-{B}\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}$
36 35 sumeq2sdv ${⊢}{y}={x}-{B}\to \sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{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}}$
37 25 32 33 36 fmptco ${⊢}{\phi }\to \left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\circ \left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)=\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)$
38 10 37 eqtr4d ${⊢}{\phi }\to {T}=\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\circ \left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)$
39 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
40 39 subrgss ${⊢}{D}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to {D}\subseteq ℂ$
41 7 40 syl ${⊢}{\phi }\to {D}\subseteq ℂ$
42 41 4 9 elplyd ${⊢}{\phi }\to \left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\in \mathrm{Poly}\left({D}\right)$
43 cnfld1 ${⊢}1={1}_{{ℂ}_{\mathrm{fld}}}$
44 43 subrg1cl ${⊢}{D}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to 1\in {D}$
45 7 44 syl ${⊢}{\phi }\to 1\in {D}$
46 plyid ${⊢}\left({D}\subseteq ℂ\wedge 1\in {D}\right)\to {X}^{p}\in \mathrm{Poly}\left({D}\right)$
47 41 45 46 syl2anc ${⊢}{\phi }\to {X}^{p}\in \mathrm{Poly}\left({D}\right)$
48 plyconst ${⊢}\left({D}\subseteq ℂ\wedge {B}\in {D}\right)\to ℂ×\left\{{B}\right\}\in \mathrm{Poly}\left({D}\right)$
49 41 8 48 syl2anc ${⊢}{\phi }\to ℂ×\left\{{B}\right\}\in \mathrm{Poly}\left({D}\right)$
50 subrgsubg ${⊢}{D}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to {D}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
51 7 50 syl ${⊢}{\phi }\to {D}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
52 cnfldadd ${⊢}+={+}_{{ℂ}_{\mathrm{fld}}}$
53 52 subgcl ${⊢}\left({D}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge {u}\in {D}\wedge {v}\in {D}\right)\to {u}+{v}\in {D}$
54 53 3expb ${⊢}\left({D}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge \left({u}\in {D}\wedge {v}\in {D}\right)\right)\to {u}+{v}\in {D}$
55 51 54 sylan ${⊢}\left({\phi }\wedge \left({u}\in {D}\wedge {v}\in {D}\right)\right)\to {u}+{v}\in {D}$
56 cnfldmul ${⊢}×={\cdot }_{{ℂ}_{\mathrm{fld}}}$
57 56 subrgmcl ${⊢}\left({D}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {u}\in {D}\wedge {v}\in {D}\right)\to {u}{v}\in {D}$
58 57 3expb ${⊢}\left({D}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge \left({u}\in {D}\wedge {v}\in {D}\right)\right)\to {u}{v}\in {D}$
59 7 58 sylan ${⊢}\left({\phi }\wedge \left({u}\in {D}\wedge {v}\in {D}\right)\right)\to {u}{v}\in {D}$
60 ax-1cn ${⊢}1\in ℂ$
61 cnfldneg ${⊢}1\in ℂ\to {inv}_{g}\left({ℂ}_{\mathrm{fld}}\right)\left(1\right)=-1$
62 60 61 ax-mp ${⊢}{inv}_{g}\left({ℂ}_{\mathrm{fld}}\right)\left(1\right)=-1$
63 eqid ${⊢}{inv}_{g}\left({ℂ}_{\mathrm{fld}}\right)={inv}_{g}\left({ℂ}_{\mathrm{fld}}\right)$
64 63 subginvcl ${⊢}\left({D}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge 1\in {D}\right)\to {inv}_{g}\left({ℂ}_{\mathrm{fld}}\right)\left(1\right)\in {D}$
65 51 45 64 syl2anc ${⊢}{\phi }\to {inv}_{g}\left({ℂ}_{\mathrm{fld}}\right)\left(1\right)\in {D}$
66 62 65 eqeltrrid ${⊢}{\phi }\to -1\in {D}$
67 47 49 55 59 66 plysub ${⊢}{\phi }\to {X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\in \mathrm{Poly}\left({D}\right)$
68 42 67 55 59 plyco ${⊢}{\phi }\to \left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\circ \left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)\in \mathrm{Poly}\left({D}\right)$
69 38 68 eqeltrd ${⊢}{\phi }\to {T}\in \mathrm{Poly}\left({D}\right)$
70 38 fveq2d ${⊢}{\phi }\to \mathrm{deg}\left({T}\right)=\mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\circ \left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)\right)$
71 eqid ${⊢}\mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)=\mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)$
72 eqid ${⊢}\mathrm{deg}\left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)=\mathrm{deg}\left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)$
73 71 72 42 67 dgrco ${⊢}{\phi }\to \mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\circ \left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)\right)=\mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)\mathrm{deg}\left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)$
74 eqid ${⊢}{X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)={X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)$
75 74 plyremlem ${⊢}{B}\in ℂ\to \left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\in \mathrm{Poly}\left(ℂ\right)\wedge \mathrm{deg}\left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)=1\wedge {\left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)}^{-1}\left[\left\{0\right\}\right]=\left\{{B}\right\}\right)$
76 23 75 syl ${⊢}{\phi }\to \left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\in \mathrm{Poly}\left(ℂ\right)\wedge \mathrm{deg}\left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)=1\wedge {\left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)}^{-1}\left[\left\{0\right\}\right]=\left\{{B}\right\}\right)$
77 76 simp2d ${⊢}{\phi }\to \mathrm{deg}\left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)=1$
78 77 oveq2d ${⊢}{\phi }\to \mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)\mathrm{deg}\left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)=\mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)\cdot 1$
79 dgrcl ${⊢}\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\in \mathrm{Poly}\left({D}\right)\to \mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)\in {ℕ}_{0}$
80 42 79 syl ${⊢}{\phi }\to \mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)\in {ℕ}_{0}$
81 80 nn0cnd ${⊢}{\phi }\to \mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)\in ℂ$
82 81 mulid1d ${⊢}{\phi }\to \mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)\cdot 1=\mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)$
83 78 82 eqtrd ${⊢}{\phi }\to \mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)\mathrm{deg}\left({X}^{p}{-}_{f}\left(ℂ×\left\{{B}\right\}\right)\right)=\mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)$
84 70 73 83 3eqtrd ${⊢}{\phi }\to \mathrm{deg}\left({T}\right)=\mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)$
85 1 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {S}\in \left\{ℝ,ℂ\right\}$
86 15 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
87 elfznn0 ${⊢}{k}\in \left(0\dots {N}\right)\to {k}\in {ℕ}_{0}$
88 87 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}\in {ℕ}_{0}$
89 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)⟶ℂ$
90 85 86 88 89 syl3anc ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟶ℂ$
91 simpr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}\in \left(0\dots {N}\right)$
92 dvn2bss ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
93 85 86 91 92 syl3anc ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
94 5 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
95 93 94 sseldd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
96 90 95 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)\in ℂ$
97 88 faccld ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}!\in ℕ$
98 97 nncnd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}!\in ℂ$
99 97 nnne0d ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}!\ne 0$
100 96 98 99 divcld ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\in ℂ$
101 42 4 100 33 dgrle ${⊢}{\phi }\to \mathrm{deg}\left(\left({y}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){{y}}^{{k}}\right)\right)\le {N}$
102 84 101 eqbrtrd ${⊢}{\phi }\to \mathrm{deg}\left({T}\right)\le {N}$
103 69 102 jca ${⊢}{\phi }\to \left({T}\in \mathrm{Poly}\left({D}\right)\wedge \mathrm{deg}\left({T}\right)\le {N}\right)$