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

Definition df-fallfac 14038
Description: Define the falling factorial function. This is the function  ( A  x.  ( A  -  1
)  x.  ... ( A  -  N )
) for complex  A and nonnegative integers  N. (Contributed by Scott Fenton, 5-Jan-2018.)
Assertion
Ref Expression
df-fallfac  |- FallFac  =  ( x  e.  CC ,  n  e.  NN0  |->  prod_ k  e.  ( 0 ... (
n  -  1 ) ) ( x  -  k ) )
Distinct variable group:    x, n, k

Detailed syntax breakdown of Definition df-fallfac
StepHypRef Expression
1 cfallfac 14035 . 2  class FallFac
2 vx . . 3  setvar  x
3 vn . . 3  setvar  n
4 cc 9536 . . 3  class  CC
5 cn0 10869 . . 3  class  NN0
6 cc0 9538 . . . . 5  class  0
73cv 1436 . . . . . 6  class  n
8 c1 9539 . . . . . 6  class  1
9 cmin 9859 . . . . . 6  class  -
107, 8, 9co 6305 . . . . 5  class  ( n  -  1 )
11 cfz 11782 . . . . 5  class  ...
126, 10, 11co 6305 . . . 4  class  ( 0 ... ( n  - 
1 ) )
132cv 1436 . . . . 5  class  x
14 vk . . . . . 6  setvar  k
1514cv 1436 . . . . 5  class  k
1613, 15, 9co 6305 . . . 4  class  ( x  -  k )
1712, 16, 14cprod 13937 . . 3  class  prod_ k  e.  ( 0 ... (
n  -  1 ) ) ( x  -  k )
182, 3, 4, 5, 17cmpt2 6307 . 2  class  ( x  e.  CC ,  n  e.  NN0  |->  prod_ k  e.  ( 0 ... ( n  -  1 ) ) ( x  -  k
) )
191, 18wceq 1437 1  wff FallFac  =  ( x  e.  CC ,  n  e.  NN0  |->  prod_ k  e.  ( 0 ... (
n  -  1 ) ) ( x  -  k ) )
Colors of variables: wff setvar class
This definition is referenced by:  fallfacval  14040
  Copyright terms: Public domain W3C validator