# Metamath Proof Explorer

## Theorem taylplem1

Description: Lemma for taylpfval and similar theorems. (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)$
Assertion taylplem1 ${⊢}\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)$

### 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 0z ${⊢}0\in ℤ$
7 4 nn0zd ${⊢}{\phi }\to {N}\in ℤ$
8 fzval2 ${⊢}\left(0\in ℤ\wedge {N}\in ℤ\right)\to \left(0\dots {N}\right)=\left[0,{N}\right]\cap ℤ$
9 6 7 8 sylancr ${⊢}{\phi }\to \left(0\dots {N}\right)=\left[0,{N}\right]\cap ℤ$
10 9 eleq2d ${⊢}{\phi }\to \left({k}\in \left(0\dots {N}\right)↔{k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)$
11 10 biimpar ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}\in \left(0\dots {N}\right)$
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 1 15 jca ${⊢}{\phi }\to \left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)$
17 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)$
18 17 3expa ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\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)$
19 16 18 sylan ${⊢}\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)$
20 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)$
21 19 20 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)$
22 11 21 syldan ${⊢}\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)$