Definition df-fallfac 14738

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

Assertion

Ref	Expression
df-fallfac	|- FallFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) )

Distinct variable group:   x, n, k

Detailed syntax breakdown of Definition df-fallfac

Step	Hyp	Ref	Expression
1		cfallfac 14735	. 2 class FallFac
2		vx	. . 3 setvar x
3		vn	. . 3 setvar n
4		cc 9934	. . 3 class CC
5		cn0 11292	. . 3 class NN0
6		cc0 9936	. . . . 5 class 0
7	3	cv 1482	. . . . . 6 class n
8		c1 9937	. . . . . 6 class 1
9		cmin 10266	. . . . . 6 class -
10	7, 8, 9	co 6650	. . . . 5 class ( n - 1 )
11		cfz 12326	. . . . 5 class ...
12	6, 10, 11	co 6650	. . . 4 class ( 0 ... ( n - 1 ) )
13	2	cv 1482	. . . . 5 class x
14		vk	. . . . . 6 setvar k
15	14	cv 1482	. . . . 5 class k
16	13, 15, 9	co 6650	. . . 4 class ( x - k )
17	12, 16, 14	cprod 14635	. . 3 class prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k )
18	2, 3, 4, 5, 17	cmpt2 6652	. 2 class ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) )
19	1, 18	wceq 1483	1 wff FallFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) )

This definition is referenced by:  fallfacval  14740