Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dvn Structured version   Unicode version

Definition df-dvn 19757
 Description: Define the -th derivative operator on functions on the complexes. This just iterates the derivative operation according to the last argument. (Contributed by Mario Carneiro, 11-Feb-2015.)
Assertion
Ref Expression
df-dvn
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-dvn
StepHypRef Expression
1 cdvn 19753 . 2
2 vs . . 3
3 vf . . 3
4 cc 8990 . . . 4
54cpw 3801 . . 3
62cv 1652 . . . 4
7 cpm 7021 . . . 4
84, 6, 7co 6083 . . 3
9 vx . . . . . 6
10 cvv 2958 . . . . . 6
119cv 1652 . . . . . . 7
12 cdv 19752 . . . . . . 7
136, 11, 12co 6083 . . . . . 6
149, 10, 13cmpt 4268 . . . . 5
15 c1st 6349 . . . . 5
1614, 15ccom 4884 . . . 4
17 cn0 10223 . . . . 5
183cv 1652 . . . . . 6
1918csn 3816 . . . . 5
2017, 19cxp 4878 . . . 4
21 cc0 8992 . . . 4
2216, 20, 21cseq 11325 . . 3
232, 3, 5, 8, 22cmpt2 6085 . 2
241, 23wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  dvnfval  19810
 Copyright terms: Public domain W3C validator