Definition df-fallfac 16004

Description: Define the falling factorial function. This is the function (𝐴 · (𝐴 − 1) · ...(𝐴 − 𝑁)) for complex 𝐴 and nonnegative integers 𝑁. (Contributed by Scott Fenton, 5-Jan-2018.)

Assertion

Ref	Expression
df-fallfac	⊢ FallFac = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘))

Distinct variable group:   𝑥,𝑛,𝑘

Detailed syntax breakdown of Definition df-fallfac

Step	Hyp	Ref	Expression
1		cfallfac 16001	. 2 class FallFac
2		vx	. . 3 setvar 𝑥
3		vn	. . 3 setvar 𝑛
4		cc 11152	. . 3 class ℂ
5		cn0 12519	. . 3 class ℕ0
6		cc0 11154	. . . . 5 class 0
7	3	cv 1532	. . . . . 6 class 𝑛
8		c1 11155	. . . . . 6 class 1
9		cmin 11490	. . . . . 6 class −
10	7, 8, 9	co 7423	. . . . 5 class (𝑛 − 1)
11		cfz 13533	. . . . 5 class ...
12	6, 10, 11	co 7423	. . . 4 class (0...(𝑛 − 1))
13	2	cv 1532	. . . . 5 class 𝑥
14		vk	. . . . . 6 setvar 𝑘
15	14	cv 1532	. . . . 5 class 𝑘
16	13, 15, 9	co 7423	. . . 4 class (𝑥 − 𝑘)
17	12, 16, 14	cprod 15902	. . 3 class ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘)
18	2, 3, 4, 5, 17	cmpo 7425	. 2 class (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘))
19	1, 18	wceq 1533	1 wff FallFac = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘))

This definition is referenced by:  fallfacval  16006