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=\left(x\in ℂ,n\in {\mathbb{N}}_0⟼\prod _{k=0}^{n-1}\left(x-k\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfallfac	$$classFallFac$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		vn	$$setvarn$$
4		cn0	$$class{\mathbb{N}}_0$$
5		vk	$$setvark$$
6		cc0	$$class0$$
7		cfz	$$class\dots$$
8	3	cv	$$setvarn$$
9		cmin	$$class-$$
10		c1	$$class1$$
11	8 10 9	co	$$class\left(n-1\right)$$
12	6 11 7	co	$$class\left(0\dots n-1\right)$$
13	1	cv	$$setvarx$$
14	5	cv	$$setvark$$
15	13 14 9	co	$$class\left(x-k\right)$$
16	12 15 5	cprod	$$class\prod _{k=0}^{n-1}\left(x-k\right)$$
17	1 3 2 4 16	cmpo	$$class\left(x\in ℂ,n\in {\mathbb{N}}_0⟼\prod _{k=0}^{n-1}\left(x-k\right)\right)$$
18	0 17	wceq	$$wffFallFac=\left(x\in ℂ,n\in {\mathbb{N}}_0⟼\prod _{k=0}^{n-1}\left(x-k\right)\right)$$