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 ) ) |
| 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 ) ) |