Definition df-fallfac 16179

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 16176	. 2 class FallFac
2		vx	. . 3 setvar 𝑥
3		vn	. . 3 setvar 𝑛
4		cc 11201	. . 3 class ℂ
5		cn0 12609	. . 3 class ℕ0
6		cc0 11203	. . . . 5 class 0
7	3	cv 1568	. . . . . 6 class 𝑛
8		c1 11204	. . . . . 6 class 1
9		cmin 11544	. . . . . 6 class −
10	7, 8, 9	co 7420	. . . . 5 class (𝑛 − 1)
11		cfz 13642	. . . . 5 class ...
12	6, 10, 11	co 7420	. . . 4 class (0...(𝑛 − 1))
13	2	cv 1568	. . . . 5 class 𝑥
14		vk	. . . . . 6 setvar 𝑘
15	14	cv 1568	. . . . 5 class 𝑘
16	13, 15, 9	co 7420	. . . 4 class (𝑥 − 𝑘)
17	12, 16, 14	cprod 16077	. . 3 class ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘)
18	2, 3, 4, 5, 17	cmpo 7422	. 2 class (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘))
19	1, 18	wceq 1569	1 wff FallFac = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘))

This definition is used by:  fallfacval  16181