Metamath Proof Explorer


Definition df-fallfac

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 , n 0 k = 0 n 1 x k

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfallfac class FallFac
1 vx setvar x
2 cc class
3 vn setvar n
4 cn0 class 0
5 vk setvar k
6 cc0 class 0
7 cfz class
8 3 cv setvar n
9 cmin class
10 c1 class 1
11 8 10 9 co class n 1
12 6 11 7 co class 0 n 1
13 1 cv setvar x
14 5 cv setvar k
15 13 14 9 co class x k
16 12 15 5 cprod class k = 0 n 1 x k
17 1 3 2 4 16 cmpo class x , n 0 k = 0 n 1 x k
18 0 17 wceq wff FallFac = x , n 0 k = 0 n 1 x k