Definition df-dvn 25041

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 25037	. 2 class D𝑛
2		vs	. . 3 setvar 𝑠
3		vf	. . 3 setvar 𝑓
4		cc 10878	. . . 4 class ℂ
5	4	cpw 4534	. . 3 class 𝒫 ℂ
6	2	cv 1538	. . . 4 class 𝑠
7		cpm 8625	. . . 4 class ↑pm
8	4, 6, 7	co 7284	. . 3 class (ℂ ↑pm 𝑠)
9		vx	. . . . . 6 setvar 𝑥
10		cvv 3433	. . . . . 6 class V
11	9	cv 1538	. . . . . . 7 class 𝑥
12		cdv 25036	. . . . . . 7 class D
13	6, 11, 12	co 7284	. . . . . 6 class (𝑠 D 𝑥)
14	9, 10, 13	cmpt 5158	. . . . 5 class (𝑥 ∈ V ↦ (𝑠 D 𝑥))
15		c1st 7838	. . . . 5 class 1st
16	14, 15	ccom 5594	. . . 4 class ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st )
17		cn0 12242	. . . . 5 class ℕ0
18	3	cv 1538	. . . . . 6 class 𝑓
19	18	csn 4562	. . . . 5 class {𝑓}
20	17, 19	cxp 5588	. . . 4 class (ℕ0 × {𝑓})
21		cc0 10880	. . . 4 class 0
22	16, 20, 21	cseq 13730	. . 3 class seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))
23	2, 3, 5, 8, 22	cmpo 7286	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
24	1, 23	wceq 1539	1 wff D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))

This definition is referenced by:  dvnfval  25095