dvn0

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

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

Step	Hyp	Ref	Expression
1		eqid	$⊢ (x \in V ⟼ S D x) = (x \in V ⟼ S D x)$
2	1	dvnfval	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to S D^{n} F = seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\}))$
3	2	fveq1d	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0) = seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (0)$
4		0z	$⊢ 0 \in ℤ$
5		simpr	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
6		0nn0	$⊢ 0 \in ℕ_{0}$
7		fvconst2g	$⊢ (F \in (ℂ ↑_{𝑝𝑚} S) \land 0 \in ℕ_{0}) \to (ℕ_{0} \times \{F\}) (0) = F$
8	5 6 7	sylancl	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (ℕ_{0} \times \{F\}) (0) = F$
9	4 8	seq1i	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (0) = F$
10	3 9	eqtrd	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0) = F$

Metamath Proof Explorer