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

Metamath Proof Explorer

Definition df-dvn

Description: Define the n -th derivative operator on functions on the complex numbers. This just iterates the derivative operation according to the last argument. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion df-dvn D𝑛 = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdvn ⊢ D𝑛
1 vs ⊢ 𝑠
2 cc ⊢ ℂ
3 2 cpw ⊢ 𝒫 ℂ
4 vf ⊢ 𝑓
5 cpm ⊢ ↑pm
6 1 cv ⊢ 𝑠
7 2 6 5 co ⊢ ( ℂ ↑pm 𝑠 )
8 cc0 ⊢ 0
9 vx ⊢ 𝑥
10 cvv ⊢ V
11 cdv ⊢ D
12 9 cv ⊢ 𝑥
13 6 12 11 co ⊢ ( 𝑠 D 𝑥 )
14 9 10 13 cmpt ⊢ ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) )
15 c1st ⊢ 1st
16 14 15 ccom ⊢ ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st )
17 cn0 ⊢ ℕ0
18 4 cv ⊢ 𝑓
19 18 csn ⊢ { 𝑓 }
20 17 19 cxp ⊢ ( ℕ0 × { 𝑓 } )
21 16 20 8 cseq ⊢ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) )
22 1 4 3 7 21 cmpo ⊢ ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) )
23 0 22 wceq ⊢ D𝑛 = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) )