# Metamath Proof Explorer

## Theorem dvnbss

Description: The set of N-times differentiable points is a subset of the domain of the function. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion 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}$

### Proof

Step Hyp Ref Expression
1 dvnff ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to \left({S}{D}^{n}{F}\right):{ℕ}_{0}⟶ℂ{↑}_{𝑝𝑚}\mathrm{dom}{F}$
2 1 ffvelrnda ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {N}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({N}\right)\in \left(ℂ{↑}_{𝑝𝑚}\mathrm{dom}{F}\right)$
3 2 3impa ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({N}\right)\in \left(ℂ{↑}_{𝑝𝑚}\mathrm{dom}{F}\right)$
4 cnex ${⊢}ℂ\in \mathrm{V}$
5 simp2 ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
6 5 dmexd ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to \mathrm{dom}{F}\in \mathrm{V}$
7 elpm2g ${⊢}\left(ℂ\in \mathrm{V}\wedge \mathrm{dom}{F}\in \mathrm{V}\right)\to \left(\left({S}{D}^{n}{F}\right)\left({N}\right)\in \left(ℂ{↑}_{𝑝𝑚}\mathrm{dom}{F}\right)↔\left(\left({S}{D}^{n}{F}\right)\left({N}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)⟶ℂ\wedge \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq \mathrm{dom}{F}\right)\right)$
8 4 6 7 sylancr ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to \left(\left({S}{D}^{n}{F}\right)\left({N}\right)\in \left(ℂ{↑}_{𝑝𝑚}\mathrm{dom}{F}\right)↔\left(\left({S}{D}^{n}{F}\right)\left({N}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)⟶ℂ\wedge \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq \mathrm{dom}{F}\right)\right)$
9 3 8 mpbid ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to \left(\left({S}{D}^{n}{F}\right)\left({N}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)⟶ℂ\wedge \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq \mathrm{dom}{F}\right)$
10 9 simprd ${⊢}\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}$