Definition df-dvn 23632

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.)

Assertion

Ref	Expression
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 } ) ) )

Distinct variable group:   f, s, x

Detailed syntax breakdown of Definition df-dvn

Step	Hyp	Ref	Expression
1		cdvn 23628	. 2 class Dn
2		vs	. . 3 setvar s
3		vf	. . 3 setvar f
4		cc 9934	. . . 4 class CC
5	4	cpw 4158	. . 3 class ~P CC
6	2	cv 1482	. . . 4 class s
7		cpm 7858	. . . 4 class ^pm
8	4, 6, 7	co 6650	. . 3 class ( CC ^pm s )
9		vx	. . . . . 6 setvar x
10		cvv 3200	. . . . . 6 class _V
11	9	cv 1482	. . . . . . 7 class x
12		cdv 23627	. . . . . . 7 class _D
13	6, 11, 12	co 6650	. . . . . 6 class ( s _D x )
14	9, 10, 13	cmpt 4729	. . . . 5 class ( x e. _V |-> ( s _D x ) )
15		c1st 7166	. . . . 5 class 1st
16	14, 15	ccom 5118	. . . 4 class ( ( x e. _V |-> ( s _D x ) ) o. 1st )
17		cn0 11292	. . . . 5 class NN0
18	3	cv 1482	. . . . . 6 class f
19	18	csn 4177	. . . . 5 class { f }
20	17, 19	cxp 5112	. . . 4 class ( NN0 X. { f } )
21		cc0 9936	. . . 4 class 0
22	16, 20, 21	cseq 12801	. . 3 class seq 0 ( ( ( x e. _V |-> ( s _D x ) ) o. 1st ) , ( NN0 X. { f } ) )
23	2, 3, 5, 8, 22	cmpt2 6652	. 2 class ( s e. ~P CC , f e. ( CC ^pm s ) |-> seq 0 ( ( ( x e. _V |-> ( s _D x ) ) o. 1st ) , ( NN0 X. { f } ) ) )
24	1, 23	wceq 1483	1 wff Dn = ( s e. ~P CC , f e. ( CC ^pm s ) |-> seq 0 ( ( ( x e. _V |-> ( s _D x ) ) o. 1st ) , ( NN0 X. { f } ) ) )

This definition is referenced by:  dvnfval  23685