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

Definition df-dvn 22035
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
StepHypRef Expression
1 cdvn 22031 . 2  class  Dn
2 vs . . 3  setvar  s
3 vf . . 3  setvar  f
4 cc 9490 . . . 4  class  CC
54cpw 4010 . . 3  class  ~P CC
62cv 1378 . . . 4  class  s
7 cpm 7421 . . . 4  class  ^pm
84, 6, 7co 6284 . . 3  class  ( CC 
^pm  s )
9 vx . . . . . 6  setvar  x
10 cvv 3113 . . . . . 6  class  _V
119cv 1378 . . . . . . 7  class  x
12 cdv 22030 . . . . . . 7  class  _D
136, 11, 12co 6284 . . . . . 6  class  ( s  _D  x )
149, 10, 13cmpt 4505 . . . . 5  class  ( x  e.  _V  |->  ( s  _D  x ) )
15 c1st 6782 . . . . 5  class  1st
1614, 15ccom 5003 . . . 4  class  ( ( x  e.  _V  |->  ( s  _D  x ) )  o.  1st )
17 cn0 10795 . . . . 5  class  NN0
183cv 1378 . . . . . 6  class  f
1918csn 4027 . . . . 5  class  { f }
2017, 19cxp 4997 . . . 4  class  ( NN0 
X.  { f } )
21 cc0 9492 . . . 4  class  0
2216, 20, 21cseq 12075 . . 3  class  seq 0
( ( ( x  e.  _V  |->  ( s  _D  x ) )  o.  1st ) ,  ( NN0  X.  {
f } ) )
232, 3, 5, 8, 22cmpt2 6286 . 2  class  ( s  e.  ~P CC , 
f  e.  ( CC 
^pm  s )  |->  seq 0 ( ( ( x  e.  _V  |->  ( s  _D  x ) )  o.  1st ) ,  ( NN0  X.  { f } ) ) )
241, 23wceq 1379 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 } ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  dvnfval  22088
  Copyright terms: Public domain W3C validator