Definition df-dvn 24460

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 24456	. 2 class D𝑛
2		vs	. . 3 setvar 𝑠
3		vf	. . 3 setvar 𝑓
4		cc 10529	. . . 4 class ℂ
5	4	cpw 4539	. . 3 class 𝒫 ℂ
6	2	cv 1532	. . . 4 class 𝑠
7		cpm 8401	. . . 4 class ↑pm
8	4, 6, 7	co 7150	. . 3 class (ℂ ↑pm 𝑠)
9		vx	. . . . . 6 setvar 𝑥
10		cvv 3495	. . . . . 6 class V
11	9	cv 1532	. . . . . . 7 class 𝑥
12		cdv 24455	. . . . . . 7 class D
13	6, 11, 12	co 7150	. . . . . 6 class (𝑠 D 𝑥)
14	9, 10, 13	cmpt 5139	. . . . 5 class (𝑥 ∈ V ↦ (𝑠 D 𝑥))
15		c1st 7681	. . . . 5 class 1st
16	14, 15	ccom 5554	. . . 4 class ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st )
17		cn0 11891	. . . . 5 class ℕ0
18	3	cv 1532	. . . . . 6 class 𝑓
19	18	csn 4561	. . . . 5 class {𝑓}
20	17, 19	cxp 5548	. . . 4 class (ℕ0 × {𝑓})
21		cc0 10531	. . . 4 class 0
22	16, 20, 21	cseq 13363	. . 3 class seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))
23	2, 3, 5, 8, 22	cmpo 7152	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
24	1, 23	wceq 1533	1 wff D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))

This definition is referenced by:  dvnfval  24513