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

Definition df-risefac 27652
Description: Define the rising 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-risefac  |- RiseFac  =  ( 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-risefac
StepHypRef Expression
1 crisefac 27651 . 2  class RiseFac
2 vx . . 3  setvar  x
3 vn . . 3  setvar  n
4 cc 9390 . . 3  class  CC
5 cn0 10689 . . 3  class  NN0
6 cc0 9392 . . . . 5  class  0
73cv 1369 . . . . . 6  class  n
8 c1 9393 . . . . . 6  class  1
9 cmin 9705 . . . . . 6  class  -
107, 8, 9co 6199 . . . . 5  class  ( n  -  1 )
11 cfz 11553 . . . . 5  class  ...
126, 10, 11co 6199 . . . 4  class  ( 0 ... ( n  - 
1 ) )
132cv 1369 . . . . 5  class  x
14 vk . . . . . 6  setvar  k
1514cv 1369 . . . . 5  class  k
16 caddc 9395 . . . . 5  class  +
1713, 15, 16co 6199 . . . 4  class  ( x  +  k )
1812, 17, 14cprod 27561 . . 3  class  prod_ k  e.  ( 0 ... (
n  -  1 ) ) ( x  +  k )
192, 3, 4, 5, 18cmpt2 6201 . 2  class  ( x  e.  CC ,  n  e.  NN0  |->  prod_ k  e.  ( 0 ... ( n  -  1 ) ) ( x  +  k ) )
201, 19wceq 1370 1  wff RiseFac  =  ( 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:  risefacval  27654
  Copyright terms: Public domain W3C validator