Definition df-dvn 24468

Description: Define the 𝑛-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.)

Assertion

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

Distinct variable group:   𝑓,𝑠,𝑥

Detailed syntax breakdown of Definition df-dvn

Step	Hyp	Ref	Expression
1		cdvn 24464	. 2 class D𝑛
2		vs	. . 3 setvar 𝑠
3		vf	. . 3 setvar 𝑓
4		cc 10537	. . . 4 class ℂ
5	4	cpw 4541	. . 3 class 𝒫 ℂ
6	2	cv 1536	. . . 4 class 𝑠
7		cpm 8409	. . . 4 class ↑pm
8	4, 6, 7	co 7158	. . 3 class (ℂ ↑pm 𝑠)
9		vx	. . . . . 6 setvar 𝑥
10		cvv 3496	. . . . . 6 class V
11	9	cv 1536	. . . . . . 7 class 𝑥
12		cdv 24463	. . . . . . 7 class D
13	6, 11, 12	co 7158	. . . . . 6 class (𝑠 D 𝑥)
14	9, 10, 13	cmpt 5148	. . . . 5 class (𝑥 ∈ V ↦ (𝑠 D 𝑥))
15		c1st 7689	. . . . 5 class 1st
16	14, 15	ccom 5561	. . . 4 class ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st )
17		cn0 11900	. . . . 5 class ℕ0
18	3	cv 1536	. . . . . 6 class 𝑓
19	18	csn 4569	. . . . 5 class {𝑓}
20	17, 19	cxp 5555	. . . 4 class (ℕ0 × {𝑓})
21		cc0 10539	. . . 4 class 0
22	16, 20, 21	cseq 13372	. . 3 class seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))
23	2, 3, 5, 8, 22	cmpo 7160	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
24	1, 23	wceq 1537	1 wff D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))

This definition is referenced by:  dvnfval  24521