Definition df-dvn 23632

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 23628	. 2 class D𝑛
2		vs	. . 3 setvar 𝑠
3		vf	. . 3 setvar 𝑓
4		cc 9934	. . . 4 class ℂ
5	4	cpw 4158	. . 3 class 𝒫 ℂ
6	2	cv 1482	. . . 4 class 𝑠
7		cpm 7858	. . . 4 class ↑pm
8	4, 6, 7	co 6650	. . 3 class (ℂ ↑pm 𝑠)
9		vx	. . . . . 6 setvar 𝑥
10		cvv 3200	. . . . . 6 class V
11	9	cv 1482	. . . . . . 7 class 𝑥
12		cdv 23627	. . . . . . 7 class D
13	6, 11, 12	co 6650	. . . . . 6 class (𝑠 D 𝑥)
14	9, 10, 13	cmpt 4729	. . . . 5 class (𝑥 ∈ V ↦ (𝑠 D 𝑥))
15		c1st 7166	. . . . 5 class 1st
16	14, 15	ccom 5118	. . . 4 class ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st )
17		cn0 11292	. . . . 5 class ℕ0
18	3	cv 1482	. . . . . 6 class 𝑓
19	18	csn 4177	. . . . 5 class {𝑓}
20	17, 19	cxp 5112	. . . 4 class (ℕ0 × {𝑓})
21		cc0 9936	. . . 4 class 0
22	16, 20, 21	cseq 12801	. . 3 class seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))
23	2, 3, 5, 8, 22	cmpt2 6652	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
24	1, 23	wceq 1483	1 wff D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))

This definition is referenced by:  dvnfval  23685