dvnp1

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

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

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to N \in ℕ_{0}$
2		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
3	1 2	eleqtrdi	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to N \in ℤ_{\geq 0}$
4		seqp1	$⊢ N \in ℤ_{\geq 0} \to seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N + 1) = seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N) ((x \in V ⟼ S D x) \circ 1^{st}) (ℕ_{0} \times \{F\}) (N + 1)$
5	3 4	syl	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N + 1) = seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N) ((x \in V ⟼ S D x) \circ 1^{st}) (ℕ_{0} \times \{F\}) (N + 1)$
6		fvex	$⊢ seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N) \in V$
7		fvex	$⊢ (ℕ_{0} \times \{F\}) (N + 1) \in V$
8	6 7	algrflem	$⊢ seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N) ((x \in V ⟼ S D x) \circ 1^{st}) (ℕ_{0} \times \{F\}) (N + 1) = (x \in V ⟼ S D x) (seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N))$
9	5 8	eqtrdi	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N + 1) = (x \in V ⟼ S D x) (seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N))$
10		eqid	$⊢ (x \in V ⟼ S D x) = (x \in V ⟼ S D x)$
11	10	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\}))$
12	11	3adant3	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to S D^{n} F = seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\}))$
13	12	fveq1d	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to (S D^{n} F) (N + 1) = seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N + 1)$
14		fvex	$⊢ (S D^{n} F) (N) \in V$
15		oveq2	$⊢ x = (S D^{n} F) (N) \to S D x = S D (S D^{n} F) (N)$
16		ovex	$⊢ S D (S D^{n} F) (N) \in V$
17	15 10 16	fvmpt	$⊢ (S D^{n} F) (N) \in V \to (x \in V ⟼ S D x) ((S D^{n} F) (N)) = S D (S D^{n} F) (N)$
18	14 17	ax-mp	$⊢ (x \in V ⟼ S D x) ((S D^{n} F) (N)) = S D (S D^{n} F) (N)$
19	12	fveq1d	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to (S D^{n} F) (N) = seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N)$
20	19	fveq2d	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to (x \in V ⟼ S D x) ((S D^{n} F) (N)) = (x \in V ⟼ S D x) (seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N))$
21	18 20	eqtr3id	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to S D (S D^{n} F) (N) = (x \in V ⟼ S D x) (seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) (N))$
22	9 13 21	3eqtr4d	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to (S D^{n} F) (N + 1) = S D (S D^{n} F) (N)$

Metamath Proof Explorer

Theorem dvnp1

Proof