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 n = s ∈ 𝒫 ℂ , f ∈ ℂ ↑ 𝑝𝑚 s ⟼ seq 0 x ∈ V ⟼ s D x ∘ 1 st ℕ 0 × f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdvn class D n
1 vs setvar s
2 cc class ℂ
3 2 cpw class 𝒫 ℂ
4 vf setvar f
5 cpm class ↑ 𝑝𝑚
6 1 cv setvar s
7 2 6 5 co class ℂ ↑ 𝑝𝑚 s
8 cc0 class 0
9 vx setvar x
10 cvv class V
11 cdv class D
12 9 cv setvar x
13 6 12 11 co class x s ′
14 9 10 13 cmpt class x ∈ V ⟼ s D x
15 c1st class 1 st
16 14 15 ccom class x ∈ V ⟼ s D x ∘ 1 st
17 cn0 class ℕ 0
18 4 cv setvar f
19 18 csn class f
20 17 19 cxp class ℕ 0 × f
21 16 20 8 cseq class seq 0 x ∈ V ⟼ s D x ∘ 1 st ℕ 0 × f
22 1 4 3 7 21 cmpo class s ∈ 𝒫 ℂ , f ∈ ℂ ↑ 𝑝𝑚 s ⟼ seq 0 x ∈ V ⟼ s D x ∘ 1 st ℕ 0 × f
23 0 22 wceq wff D n = s ∈ 𝒫 ℂ , f ∈ ℂ ↑ 𝑝𝑚 s ⟼ seq 0 x ∈ V ⟼ s D x ∘ 1 st ℕ 0 × f