Metamath Proof Explorer

Theorem taylfvallem1

Description: Lemma for taylfval . (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)$
Assertion 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 ℂ$

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 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {S}\in \left\{ℝ,ℂ\right\}$
7 cnex ${⊢}ℂ\in \mathrm{V}$
8 7 a1i ${⊢}{\phi }\to ℂ\in \mathrm{V}$
9 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)$
10 8 1 2 3 9 syl22anc ${⊢}{\phi }\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
11 10 ad2antrr ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
12 simpr ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}\in \left(\left[0,{N}\right]\cap ℤ\right)$
13 12 elin2d ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}\in ℤ$
14 12 elin1d ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}\in \left[0,{N}\right]$
15 0xr ${⊢}0\in {ℝ}^{*}$
16 nn0re ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℝ$
17 16 rexrd ${⊢}{N}\in {ℕ}_{0}\to {N}\in {ℝ}^{*}$
18 id ${⊢}{N}=\mathrm{+\infty }\to {N}=\mathrm{+\infty }$
19 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
20 18 19 eqeltrdi ${⊢}{N}=\mathrm{+\infty }\to {N}\in {ℝ}^{*}$
21 17 20 jaoi ${⊢}\left({N}\in {ℕ}_{0}\vee {N}=\mathrm{+\infty }\right)\to {N}\in {ℝ}^{*}$
22 4 21 syl ${⊢}{\phi }\to {N}\in {ℝ}^{*}$
23 22 ad2antrr ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {N}\in {ℝ}^{*}$
24 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)$
25 15 23 24 sylancr ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\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)$
26 14 25 mpbid ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to \left({k}\in {ℝ}^{*}\wedge 0\le {k}\wedge {k}\le {N}\right)$
27 26 simp2d ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to 0\le {k}$
28 elnn0z ${⊢}{k}\in {ℕ}_{0}↔\left({k}\in ℤ\wedge 0\le {k}\right)$
29 13 27 28 sylanbrc ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}\in {ℕ}_{0}$
30 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)⟶ℂ$
31 6 11 29 30 syl3anc ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\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)⟶ℂ$
32 5 adantlr ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\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)$
33 31 32 ffvelrnd ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\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 ℂ$
34 29 faccld ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}!\in ℕ$
35 34 nncnd ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}!\in ℂ$
36 34 nnne0d ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {k}!\ne 0$
37 33 35 36 divcld ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\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 ℂ$
38 simplr ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {X}\in ℂ$
39 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {F}:{A}⟶ℂ$
40 dvnbss ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {k}\in {ℕ}_{0}\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\subseteq \mathrm{dom}{F}$
41 6 11 29 40 syl3anc ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\subseteq \mathrm{dom}{F}$
42 39 41 fssdmd ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\subseteq {A}$
43 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
44 1 43 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
45 3 44 sstrd ${⊢}{\phi }\to {A}\subseteq ℂ$
46 45 ad2antrr ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {A}\subseteq ℂ$
47 42 46 sstrd ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)\subseteq ℂ$
48 47 32 sseldd ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {B}\in ℂ$
49 38 48 subcld ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {X}-{B}\in ℂ$
50 49 29 expcld ${⊢}\left(\left({\phi }\wedge {X}\in ℂ\right)\wedge {k}\in \left(\left[0,{N}\right]\cap ℤ\right)\right)\to {\left({X}-{B}\right)}^{{k}}\in ℂ$
51 37 50 mulcld ${⊢}\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 ℂ$