dvn1

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

		Ref	Expression
	Assertion	dvn1	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (1) = S D F$

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 \in ℕ_{0}$
4		dvnp1	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land 0 \in ℕ_{0}) \to (S D^{n} F) (0 + 1) = S D (S D^{n} F) (0)$
5	3 4	mp3an3	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0 + 1) = S D (S D^{n} F) (0)$
6		dvn0	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0) = F$
7	6	oveq2d	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to S D (S D^{n} F) (0) = S D F$
8	5 7	eqtrd	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0 + 1) = S D F$
9	2 8	eqtr3id	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (1) = S D F$

Metamath Proof Explorer