Metamath Proof Explorer

Theorem dvn1

Description: One times iterated derivative. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion dvn1 ⊢ S ⊆ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S → S D n F ⁡ 1 = S D F

Proof

Step Hyp Ref Expression
1 0p1e1 ⊢ 0 + 1 = 1
2 1 fveq2i ⊢ S D n F ⁡ 0 + 1 = S D n F ⁡ 1
3 0nn0 ⊢ 0 ∈ ℕ 0
4 dvnp1 ⊢ S ⊆ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S ∧ 0 ∈ ℕ 0 → S D n F ⁡ 0 + 1 = S D S D n F ⁡ 0
5 3 4 mp3an3 ⊢ S ⊆ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S → S D n F ⁡ 0 + 1 = S D S D n F ⁡ 0
6 dvn0 ⊢ S ⊆ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S → S D n F ⁡ 0 = F
7 6 oveq2d ⊢ S ⊆ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S → S D S D n F ⁡ 0 = S D F
8 5 7 eqtrd ⊢ S ⊆ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S → S D n F ⁡ 0 + 1 = S D F
9 2 8 eqtr3id ⊢ S ⊆ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S → S D n F ⁡ 1 = S D F