Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fallfac Structured version   Unicode version

Definition df-fallfac 29304
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 29301 . 2  class FallFac
2 vx . . 3  setvar  x
3 vn . . 3  setvar  n
4 cc 9507 . . 3  class  CC
5 cn0 10816 . . 3  class  NN0
6 cc0 9509 . . . . 5  class  0
73cv 1394 . . . . . 6  class  n
8 c1 9510 . . . . . 6  class  1
9 cmin 9824 . . . . . 6  class  -
107, 8, 9co 6296 . . . . 5  class  ( n  -  1 )
11 cfz 11697 . . . . 5  class  ...
126, 10, 11co 6296 . . . 4  class  ( 0 ... ( n  - 
1 ) )
132cv 1394 . . . . 5  class  x
14 vk . . . . . 6  setvar  k
1514cv 1394 . . . . 5  class  k
1613, 15, 9co 6296 . . . 4  class  ( x  -  k )
1712, 16, 14cprod 13723 . . 3  class  prod_ k  e.  ( 0 ... (
n  -  1 ) ) ( x  -  k )
182, 3, 4, 5, 17cmpt2 6298 . 2  class  ( x  e.  CC ,  n  e.  NN0  |->  prod_ k  e.  ( 0 ... ( n  -  1 ) ) ( x  -  k
) )
191, 18wceq 1395 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  29306
  Copyright terms: Public domain W3C validator