# Metamath Proof Explorer

Description: The N -th derivative of the M -th derivative of F is the same as the M + N -th derivative of F . (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion dvnadd ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge \left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}\right)$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{n}=0\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left(0\right)$
2 oveq2 ${⊢}{n}=0\to {M}+{n}={M}+0$
3 2 fveq2d ${⊢}{n}=0\to \left({S}{D}^{n}{F}\right)\left({M}+{n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+0\right)$
4 1 3 eqeq12d ${⊢}{n}=0\to \left(\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{n}\right)↔\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left(0\right)=\left({S}{D}^{n}{F}\right)\left({M}+0\right)\right)$
5 4 imbi2d ${⊢}{n}=0\to \left(\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{n}\right)\right)↔\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left(0\right)=\left({S}{D}^{n}{F}\right)\left({M}+0\right)\right)\right)$
6 fveq2 ${⊢}{n}={k}\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)$
7 oveq2 ${⊢}{n}={k}\to {M}+{n}={M}+{k}$
8 7 fveq2d ${⊢}{n}={k}\to \left({S}{D}^{n}{F}\right)\left({M}+{n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)$
9 6 8 eqeq12d ${⊢}{n}={k}\to \left(\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{n}\right)↔\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)\right)$
10 9 imbi2d ${⊢}{n}={k}\to \left(\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{n}\right)\right)↔\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)\right)\right)$
11 fveq2 ${⊢}{n}={k}+1\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}+1\right)$
12 oveq2 ${⊢}{n}={k}+1\to {M}+{n}={M}+{k}+1$
13 12 fveq2d ${⊢}{n}={k}+1\to \left({S}{D}^{n}{F}\right)\left({M}+{n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)$
14 11 13 eqeq12d ${⊢}{n}={k}+1\to \left(\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{n}\right)↔\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}+1\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)\right)$
15 14 imbi2d ${⊢}{n}={k}+1\to \left(\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{n}\right)\right)↔\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}+1\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)\right)\right)$
16 fveq2 ${⊢}{n}={N}\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}\right)$
17 oveq2 ${⊢}{n}={N}\to {M}+{n}={M}+{N}$
18 17 fveq2d ${⊢}{n}={N}\to \left({S}{D}^{n}{F}\right)\left({M}+{n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}\right)$
19 16 18 eqeq12d ${⊢}{n}={N}\to \left(\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{n}\right)↔\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}\right)\right)$
20 19 imbi2d ${⊢}{n}={N}\to \left(\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({n}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{n}\right)\right)↔\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}\right)\right)\right)$
21 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
22 21 ad2antrr ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to {S}\subseteq ℂ$
23 ssidd ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to ℂ\subseteq ℂ$
24 cnex ${⊢}ℂ\in \mathrm{V}$
25 elpm2g ${⊢}\left(ℂ\in \mathrm{V}\wedge {S}\in \left\{ℝ,ℂ\right\}\right)\to \left({F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)↔\left({F}:\mathrm{dom}{F}⟶ℂ\wedge \mathrm{dom}{F}\subseteq {S}\right)\right)$
26 24 25 mpan ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to \left({F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)↔\left({F}:\mathrm{dom}{F}⟶ℂ\wedge \mathrm{dom}{F}\subseteq {S}\right)\right)$
27 26 simplbda ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to \mathrm{dom}{F}\subseteq {S}$
28 24 a1i ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to ℂ\in \mathrm{V}$
29 simpl ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to {S}\in \left\{ℝ,ℂ\right\}$
30 pmss12g ${⊢}\left(\left(ℂ\subseteq ℂ\wedge \mathrm{dom}{F}\subseteq {S}\right)\wedge \left(ℂ\in \mathrm{V}\wedge {S}\in \left\{ℝ,ℂ\right\}\right)\right)\to ℂ{↑}_{𝑝𝑚}\mathrm{dom}{F}\subseteq ℂ{↑}_{𝑝𝑚}{S}$
31 23 27 28 29 30 syl22anc ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to ℂ{↑}_{𝑝𝑚}\mathrm{dom}{F}\subseteq ℂ{↑}_{𝑝𝑚}{S}$
32 31 adantr ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to ℂ{↑}_{𝑝𝑚}\mathrm{dom}{F}\subseteq ℂ{↑}_{𝑝𝑚}{S}$
33 dvnff ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to \left({S}{D}^{n}{F}\right):{ℕ}_{0}⟶ℂ{↑}_{𝑝𝑚}\mathrm{dom}{F}$
34 33 ffvelrnda ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({M}\right)\in \left(ℂ{↑}_{𝑝𝑚}\mathrm{dom}{F}\right)$
35 32 34 sseldd ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({M}\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
36 dvn0 ${⊢}\left({S}\subseteq ℂ\wedge \left({S}{D}^{n}{F}\right)\left({M}\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left(0\right)=\left({S}{D}^{n}{F}\right)\left({M}\right)$
37 22 35 36 syl2anc ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left(0\right)=\left({S}{D}^{n}{F}\right)\left({M}\right)$
38 nn0cn ${⊢}{M}\in {ℕ}_{0}\to {M}\in ℂ$
39 38 adantl ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to {M}\in ℂ$
40 39 addid1d ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to {M}+0={M}$
41 40 fveq2d ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({M}+0\right)=\left({S}{D}^{n}{F}\right)\left({M}\right)$
42 37 41 eqtr4d ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left(0\right)=\left({S}{D}^{n}{F}\right)\left({M}+0\right)$
43 oveq2 ${⊢}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)\to {S}\mathrm{D}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)$
44 22 adantr ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to {S}\subseteq ℂ$
45 35 adantr ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({M}\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
46 simpr ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
47 dvnp1 ${⊢}\left({S}\subseteq ℂ\wedge \left({S}{D}^{n}{F}\right)\left({M}\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}+1\right)={S}\mathrm{D}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)$
48 44 45 46 47 syl3anc ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}+1\right)={S}\mathrm{D}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)$
49 39 adantr ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to {M}\in ℂ$
50 nn0cn ${⊢}{k}\in {ℕ}_{0}\to {k}\in ℂ$
51 50 adantl ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in ℂ$
52 1cnd ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to 1\in ℂ$
53 49 51 52 addassd ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to {M}+{k}+1={M}+{k}+1$
54 53 fveq2d ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)$
55 simpllr ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
56 nn0addcl ${⊢}\left({M}\in {ℕ}_{0}\wedge {k}\in {ℕ}_{0}\right)\to {M}+{k}\in {ℕ}_{0}$
57 56 adantll ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to {M}+{k}\in {ℕ}_{0}$
58 dvnp1 ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}+{k}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)$
59 44 55 57 58 syl3anc ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)$
60 54 59 eqtr3d ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)$
61 48 60 eqeq12d ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}+1\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)↔{S}\mathrm{D}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)\right)$
62 43 61 syl5ibr ${⊢}\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}+1\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)\right)$
63 62 expcom ${⊢}{k}\in {ℕ}_{0}\to \left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left(\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}+1\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)\right)\right)$
64 63 a2d ${⊢}{k}\in {ℕ}_{0}\to \left(\left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}\right)\right)\to \left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}+1\right)=\left({S}{D}^{n}{F}\right)\left({M}+{k}+1\right)\right)\right)$
65 5 10 15 20 42 64 nn0ind ${⊢}{N}\in {ℕ}_{0}\to \left(\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}\right)\right)$
66 65 com12 ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({N}\in {ℕ}_{0}\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}\right)\right)$
67 66 impr ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge \left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}\right)$