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)
Ref | Expression | ||
---|---|---|---|
Assertion | df-fallfac | |- FallFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cfallfac | |- FallFac |
|
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 | 5 | cv | |- k |
15 | 13 14 9 | co | |- ( x - k ) |
16 | 12 15 5 | cprod | |- prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) |
17 | 1 3 2 4 16 | cmpo | |- ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) ) |
18 | 0 17 | wceq | |- FallFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) ) |