Metamath Proof Explorer

Theorem dvn2bss

Description: An N-times differentiable point is an M-times differentiable point, if M <_ N . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Assertion dvn2bss ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\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({M}\right)$

Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to {S}\in \left\{ℝ,ℂ\right\}$
2 simp2 ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
3 elfznn0 ${⊢}{M}\in \left(0\dots {N}\right)\to {M}\in {ℕ}_{0}$
4 3 3ad2ant3 ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to {M}\in {ℕ}_{0}$
5 elfzuz3 ${⊢}{M}\in \left(0\dots {N}\right)\to {N}\in {ℤ}_{\ge {M}}$
6 5 3ad2ant3 ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to {N}\in {ℤ}_{\ge {M}}$
7 uznn0sub ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}-{M}\in {ℕ}_{0}$
8 6 7 syl ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to {N}-{M}\in {ℕ}_{0}$
9 dvnadd ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge \left({M}\in {ℕ}_{0}\wedge {N}-{M}\in {ℕ}_{0}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}-{M}\right)$
10 1 2 4 8 9 syl22anc ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}-{M}\right)$
11 4 nn0cnd ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to {M}\in ℂ$
12 elfzuz2 ${⊢}{M}\in \left(0\dots {N}\right)\to {N}\in {ℤ}_{\ge 0}$
13 12 3ad2ant3 ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to {N}\in {ℤ}_{\ge 0}$
14 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
15 13 14 eleqtrrdi ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to {N}\in {ℕ}_{0}$
16 15 nn0cnd ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to {N}\in ℂ$
17 11 16 pncan3d ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to {M}+{N}-{M}={N}$
18 17 fveq2d ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({M}+{N}-{M}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
19 10 18 eqtrd ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
20 19 dmeqd ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
21 cnex ${⊢}ℂ\in \mathrm{V}$
22 21 a1i ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to ℂ\in \mathrm{V}$
23 dvnf ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({M}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)⟶ℂ$
24 3 23 syl3an3 ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({M}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)⟶ℂ$
25 dvnbss ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in {ℕ}_{0}\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)\subseteq \mathrm{dom}{F}$
26 3 25 syl3an3 ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)\subseteq \mathrm{dom}{F}$
27 elpmi ${⊢}{F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\to \left({F}:\mathrm{dom}{F}⟶ℂ\wedge \mathrm{dom}{F}\subseteq {S}\right)$
28 27 3ad2ant2 ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \left({F}:\mathrm{dom}{F}⟶ℂ\wedge \mathrm{dom}{F}\subseteq {S}\right)$
29 28 simprd ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \mathrm{dom}{F}\subseteq {S}$
30 26 29 sstrd ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)\subseteq {S}$
31 elpm2r ${⊢}\left(\left(ℂ\in \mathrm{V}\wedge {S}\in \left\{ℝ,ℂ\right\}\right)\wedge \left(\left({S}{D}^{n}{F}\right)\left({M}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)⟶ℂ\wedge \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)\subseteq {S}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({M}\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
32 22 1 24 30 31 syl22anc ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({M}\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
33 dvnbss ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge \left({S}{D}^{n}{F}\right)\left({M}\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}-{M}\in {ℕ}_{0}\right)\to \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)\subseteq \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)$
34 1 32 8 33 syl3anc ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in \left(0\dots {N}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)\subseteq \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)$
35 20 34 eqsstrrd ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\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({M}\right)$