Definition df-dvn 25903

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 25899	. 2 class D𝑛
2		vs	. . 3 setvar 𝑠
3		vf	. . 3 setvar 𝑓
4		cc 11153	. . . 4 class ℂ
5	4	cpw 4600	. . 3 class 𝒫 ℂ
6	2	cv 1539	. . . 4 class 𝑠
7		cpm 8867	. . . 4 class ↑pm
8	4, 6, 7	co 7431	. . 3 class (ℂ ↑pm 𝑠)
9		vx	. . . . . 6 setvar 𝑥
10		cvv 3480	. . . . . 6 class V
11	9	cv 1539	. . . . . . 7 class 𝑥
12		cdv 25898	. . . . . . 7 class D
13	6, 11, 12	co 7431	. . . . . 6 class (𝑠 D 𝑥)
14	9, 10, 13	cmpt 5225	. . . . 5 class (𝑥 ∈ V ↦ (𝑠 D 𝑥))
15		c1st 8012	. . . . 5 class 1st
16	14, 15	ccom 5689	. . . 4 class ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st )
17		cn0 12526	. . . . 5 class ℕ0
18	3	cv 1539	. . . . . 6 class 𝑓
19	18	csn 4626	. . . . 5 class {𝑓}
20	17, 19	cxp 5683	. . . 4 class (ℕ0 × {𝑓})
21		cc0 11155	. . . 4 class 0
22	16, 20, 21	cseq 14042	. . 3 class seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))
23	2, 3, 5, 8, 22	cmpo 7433	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
24	1, 23	wceq 1540	1 wff D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))

This definition is referenced by:  dvnfval  25958