dvn1

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

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

Step	Hyp	Ref	Expression
1		0p1e1	⊢ ( 0 + 1 ) = 1
2	1	fveq2i	⊢ ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ 1 )
3		0nn0	⊢ 0 ∈ ℕ₀
4		dvnp1	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 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 𝐹 ) )

Metamath Proof Explorer