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

Definition df-risefac 25275
Description: Define the rising factorial function. This is the function  ( A  x.  ( A  +  1
)  x.  ... ( A  +  N )
) for complex  A and non-negative 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 25274 . 2  class RiseFac
2 vx . . 3  set  x
3 vn . . 3  set  n
4 cc 8944 . . 3  class  CC
5 cn0 10177 . . 3  class  NN0
6 cc0 8946 . . . . 5  class  0
73cv 1648 . . . . . 6  class  n
8 c1 8947 . . . . . 6  class  1
9 cmin 9247 . . . . . 6  class  -
107, 8, 9co 6040 . . . . 5  class  ( n  -  1 )
11 cfz 10999 . . . . 5  class  ...
126, 10, 11co 6040 . . . 4  class  ( 0 ... ( n  - 
1 ) )
132cv 1648 . . . . 5  class  x
14 vk . . . . . 6  set  k
1514cv 1648 . . . . 5  class  k
16 caddc 8949 . . . . 5  class  +
1713, 15, 16co 6040 . . . 4  class  ( x  +  k )
1812, 17, 14cprod 25184 . . 3  class  prod_ k  e.  ( 0 ... (
n  -  1 ) ) ( x  +  k )
192, 3, 4, 5, 18cmpt2 6042 . 2  class  ( x  e.  CC ,  n  e.  NN0  |->  prod_ k  e.  ( 0 ... ( n  -  1 ) ) ( x  +  k ) )
201, 19wceq 1649 1  wff RiseFac  =  ( x  e.  CC ,  n  e.  NN0  |->  prod_ k  e.  ( 0 ... (
n  -  1 ) ) ( x  +  k ) )
Colors of variables: wff set class
This definition is referenced by:  risefacval  25277
  Copyright terms: Public domain W3C validator