# Metamath Proof Explorer

## Theorem dvnp1

Description: Successor iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion dvnp1 ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({N}+1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 simp3 ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to {N}\in {ℕ}_{0}$
2 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
3 1 2 eleqtrdi ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to {N}\in {ℤ}_{\ge 0}$
4 seqp1 ${⊢}{N}\in {ℤ}_{\ge 0}\to seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}+1\right)=seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}\right)\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right)\left({ℕ}_{0}×\left\{{F}\right\}\right)\left({N}+1\right)$
5 3 4 syl ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}+1\right)=seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}\right)\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right)\left({ℕ}_{0}×\left\{{F}\right\}\right)\left({N}+1\right)$
6 fvex ${⊢}seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}\right)\in \mathrm{V}$
7 fvex ${⊢}\left({ℕ}_{0}×\left\{{F}\right\}\right)\left({N}+1\right)\in \mathrm{V}$
8 6 7 algrflem ${⊢}seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}\right)\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right)\left({ℕ}_{0}×\left\{{F}\right\}\right)\left({N}+1\right)=\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\left(seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}\right)\right)$
9 5 8 eqtrdi ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}+1\right)=\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\left(seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}\right)\right)$
10 eqid ${⊢}\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)=\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)$
11 10 dvnfval ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to {S}{D}^{n}{F}=seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)$
12 11 3adant3 ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to {S}{D}^{n}{F}=seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)$
13 12 fveq1d ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({N}+1\right)=seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}+1\right)$
14 fvex ${⊢}\left({S}{D}^{n}{F}\right)\left({N}\right)\in \mathrm{V}$
15 oveq2 ${⊢}{x}=\left({S}{D}^{n}{F}\right)\left({N}\right)\to {S}\mathrm{D}{x}={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}\right)$
16 ovex ${⊢}{S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}\right)\in \mathrm{V}$
17 15 10 16 fvmpt ${⊢}\left({S}{D}^{n}{F}\right)\left({N}\right)\in \mathrm{V}\to \left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\left(\left({S}{D}^{n}{F}\right)\left({N}\right)\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}\right)$
18 14 17 ax-mp ${⊢}\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\left(\left({S}{D}^{n}{F}\right)\left({N}\right)\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}\right)$
19 12 fveq1d ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({N}\right)=seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}\right)$
20 19 fveq2d ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to \left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\left(\left({S}{D}^{n}{F}\right)\left({N}\right)\right)=\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\left(seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}\right)\right)$
21 18 20 syl5eqr ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to {S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}\right)=\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\left(seq0\left(\left(\left({x}\in \mathrm{V}⟼{S}\mathrm{D}{x}\right)\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{F}\right\}\right)\right)\left({N}\right)\right)$
22 9 13 21 3eqtr4d ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({N}+1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}\right)$