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 27677
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 27674 . 2  class FallFac
2 vx . . 3  setvar  x
3 vn . . 3  setvar  n
4 cc 9395 . . 3  class  CC
5 cn0 10694 . . 3  class  NN0
6 cc0 9397 . . . . 5  class  0
73cv 1369 . . . . . 6  class  n
8 c1 9398 . . . . . 6  class  1
9 cmin 9710 . . . . . 6  class  -
107, 8, 9co 6203 . . . . 5  class  ( n  -  1 )
11 cfz 11558 . . . . 5  class  ...
126, 10, 11co 6203 . . . 4  class  ( 0 ... ( n  - 
1 ) )
132cv 1369 . . . . 5  class  x
14 vk . . . . . 6  setvar  k
1514cv 1369 . . . . 5  class  k
1613, 15, 9co 6203 . . . 4  class  ( x  -  k )
1712, 16, 14cprod 27585 . . 3  class  prod_ k  e.  ( 0 ... (
n  -  1 ) ) ( x  -  k )
182, 3, 4, 5, 17cmpt2 6205 . 2  class  ( x  e.  CC ,  n  e.  NN0  |->  prod_ k  e.  ( 0 ... ( n  -  1 ) ) ( x  -  k
) )
191, 18wceq 1370 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  27679
  Copyright terms: Public domain W3C validator