Metamath Proof Explorer


Definition df-risefac

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)

Ref Expression
Assertion df-risefac
|- RiseFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crisefac
 |-  RiseFac
1 vx
 |-  x
2 cc
 |-  CC
3 vn
 |-  n
4 cn0
 |-  NN0
5 vk
 |-  k
6 cc0
 |-  0
7 cfz
 |-  ...
8 3 cv
 |-  n
9 cmin
 |-  -
10 c1
 |-  1
11 8 10 9 co
 |-  ( n - 1 )
12 6 11 7 co
 |-  ( 0 ... ( n - 1 ) )
13 1 cv
 |-  x
14 caddc
 |-  +
15 5 cv
 |-  k
16 13 15 14 co
 |-  ( x + k )
17 12 16 5 cprod
 |-  prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k )
18 1 3 2 4 17 cmpo
 |-  ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k ) )
19 0 18 wceq
 |-  RiseFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k ) )