Metamath Proof Explorer


Theorem dvn1

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

Ref Expression
Assertion dvn1 ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) = ( 𝑆 D 𝐹 ) )

Proof

Step Hyp Ref Expression
1 0p1e1 ( 0 + 1 ) = 1
2 1 fveq2i ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 )
3 0nn0 0 ∈ ℕ0
4 dvnp1 ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 0 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) )
5 3 4 mp3an3 ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) )
6 dvn0 ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
7 6 oveq2d ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) = ( 𝑆 D 𝐹 ) )
8 5 7 eqtrd ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( 𝑆 D 𝐹 ) )
9 2 8 eqtr3id ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) = ( 𝑆 D 𝐹 ) )