Metamath Proof Explorer

Theorem taylply

Description: The Taylor polynomial is a polynomial of degree (at most) N . (Contributed by Mario Carneiro, 31-Dec-2016)

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}$
Assertion taylply ${⊢}{\phi }\to \left({T}\in \mathrm{Poly}\left(ℂ\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 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
8 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
9 8 subrgid ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to ℂ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$
10 7 9 mp1i ${⊢}{\phi }\to ℂ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$
11 cnex ${⊢}ℂ\in \mathrm{V}$
12 11 a1i ${⊢}{\phi }\to ℂ\in \mathrm{V}$
13 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)$
14 12 1 2 3 13 syl22anc ${⊢}{\phi }\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
15 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}$
16 1 14 4 15 syl3anc ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq \mathrm{dom}{F}$
17 2 16 fssdmd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq {A}$
18 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
19 1 18 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
20 3 19 sstrd ${⊢}{\phi }\to {A}\subseteq ℂ$
21 17 20 sstrd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq ℂ$
22 21 5 sseldd ${⊢}{\phi }\to {B}\in ℂ$
23 1 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {S}\in \left\{ℝ,ℂ\right\}$
24 14 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
25 elfznn0 ${⊢}{k}\in \left(0\dots {N}\right)\to {k}\in {ℕ}_{0}$
26 25 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}\in {ℕ}_{0}$
27 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)⟶ℂ$
28 23 24 26 27 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)⟶ℂ$
29 simpr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}\in \left(0\dots {N}\right)$
30 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)$
31 23 24 29 30 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)$
32 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)$
33 31 32 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)$
34 28 33 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 ℂ$
35 26 faccld ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}!\in ℕ$
36 35 nncnd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}!\in ℂ$
37 35 nnne0d ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}!\ne 0$
38 34 36 37 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 ℂ$
39 1 2 3 4 5 6 10 22 38 taylply2 ${⊢}{\phi }\to \left({T}\in \mathrm{Poly}\left(ℂ\right)\wedge \mathrm{deg}\left({T}\right)\le {N}\right)$