This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) = ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) )
2 1 dvnfval ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D𝑛 𝐹 ) = seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) )
3 2 fveq1d ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 0 ) )
4 0z ⊢ 0 ∈ ℤ
5 simpr ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
6 0nn0 ⊢ 0 ∈ ℕ0
7 fvconst2g ⊢ ( ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 0 ∈ ℕ0 ) → ( ( ℕ0 × { 𝐹 } ) ‘ 0 ) = 𝐹 )
8 5 6 7 sylancl ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( ℕ0 × { 𝐹 } ) ‘ 0 ) = 𝐹 )
9 4 8 seq1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 0 ) = 𝐹 )
10 3 9 eqtrd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )