# Metamath Proof Explorer

## Theorem taylplem2

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 taylplem2 ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({X}-{B}\right)}^{{k}}\in ℂ$

### 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 adantr ${⊢}\left({\phi }\wedge {X}\in ℂ\right)\to \left({k}\in \left(0\dots {N}\right)↔{k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)$
12 11 biimpa ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {k}\in \left(\left[0,{N}\right]\cap ℤ\right)$
13 4 orcd ${⊢}{\phi }\to \left({N}\in {ℕ}_{0}\vee {N}=\mathrm{+\infty }\right)$
14 1 2 3 4 5 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)$
15 1 2 3 13 14 taylfvallem1 ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\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({B}\right)}{{k}!}\right){\left({X}-{B}\right)}^{{k}}\in ℂ$
16 12 15 syldan ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({X}-{B}\right)}^{{k}}\in ℂ$