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	|- Dn = ( s e. ~P CC , f e. ( CC ^pm s ) |-> seq 0 ( ( ( x e. _V |-> ( s _D x ) ) o. 1st ) , ( NN0 X. { f } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdvn	|- Dn
1		vs	|- s
2		cc	|- CC
3	2	cpw	|- ~P CC
4		vf	|- f
5		cpm	|- ^pm
6	1	cv	|- s
7	2 6 5	co	|- ( CC ^pm s )
8		cc0	|- 0
9		vx	|- x
10		cvv	|- _V
11		cdv	|- _D
12	9	cv	|- x
13	6 12 11	co	|- ( s _D x )
14	9 10 13	cmpt	|- ( x e. _V |-> ( s _D x ) )
15		c1st	|- 1st
16	14 15	ccom	|- ( ( x e. _V |-> ( s _D x ) ) o. 1st )
17		cn0	|- NN0
18	4	cv	|- f
19	18	csn	|- { f }
20	17 19	cxp	|- ( NN0 X. { f } )
21	16 20 8	cseq	|- seq 0 ( ( ( x e. _V |-> ( s _D x ) ) o. 1st ) , ( NN0 X. { f } ) )
22	1 4 3 7 21	cmpo	|- ( s e. ~P CC , f e. ( CC ^pm s ) |-> seq 0 ( ( ( x e. _V |-> ( s _D x ) ) o. 1st ) , ( NN0 X. { f } ) ) )
23	0 22	wceq	|- Dn = ( s e. ~P CC , f e. ( CC ^pm s ) |-> seq 0 ( ( ( x e. _V |-> ( s _D x ) ) o. 1st ) , ( NN0 X. { f } ) ) )