Definition df-dvn

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

	Ref	Expression
Assertion	df-dvn	$$⊢D^n=\left(s\in 𝒫ℂ,f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)⟼seq0\left(\left(\left(x\in \mathrm{V}⟼s\mathrm{D}x\right)\circ 1^{st}\right),\left({\mathbb{N}}_0\times \left\{f\right\}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdvn	$$class{D}^n$$
1		vs	$$setvars$$
2		cc	$$classℂ$$
3	2	cpw	$$class𝒫ℂ$$
4		vf	$$setvarf$$
5		cpm	$$class{\uparrow }_{𝑝𝑚}$$
6	1	cv	$$setvars$$
7	2 6 5	co	$$class\left(ℂ{\uparrow }_{𝑝𝑚}s\right)$$
8		cc0	$$class0$$
9		vx	$$setvarx$$
10		cvv	$$class\mathrm{V}$$
11		cdv	$$class\mathrm{D}$$
12	9	cv	$$setvarx$$
13	6 12 11	co	$$class{x}_s^{\prime }$$
14	9 10 13	cmpt	$$class\left(x\in \mathrm{V}⟼s\mathrm{D}x\right)$$
15		c1st	$$class{1}^{st}$$
16	14 15	ccom	$$class\left(\left(x\in \mathrm{V}⟼s\mathrm{D}x\right)\circ 1^{st}\right)$$
17		cn0	$$class{\mathbb{N}}_0$$
18	4	cv	$$setvarf$$
19	18	csn	$$class\left\{f\right\}$$
20	17 19	cxp	$$class\left({\mathbb{N}}_0\times \left\{f\right\}\right)$$
21	16 20 8	cseq	$$classseq0\left(\left(\left(x\in \mathrm{V}⟼s\mathrm{D}x\right)\circ 1^{st}\right),\left({\mathbb{N}}_0\times \left\{f\right\}\right)\right)$$
22	1 4 3 7 21	cmpo	$$class\left(s\in 𝒫ℂ,f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)⟼seq0\left(\left(\left(x\in \mathrm{V}⟼s\mathrm{D}x\right)\circ 1^{st}\right),\left({\mathbb{N}}_0\times \left\{f\right\}\right)\right)\right)$$
23	0 22	wceq	$$wff{D}^n=\left(s\in 𝒫ℂ,f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)⟼seq0\left(\left(\left(x\in \mathrm{V}⟼s\mathrm{D}x\right)\circ 1^{st}\right),\left({\mathbb{N}}_0\times \left\{f\right\}\right)\right)\right)$$