Definition df-fallfac 14577

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 14574	. 2 class FallFac
2		vx	. . 3 setvar 𝑥
3		vn	. . 3 setvar 𝑛
4		cc 9813	. . 3 class ℂ
5		cn0 11169	. . 3 class ℕ0
6		cc0 9815	. . . . 5 class 0
7	3	cv 1474	. . . . . 6 class 𝑛
8		c1 9816	. . . . . 6 class 1
9		cmin 10145	. . . . . 6 class −
10	7, 8, 9	co 6549	. . . . 5 class (𝑛 − 1)
11		cfz 12197	. . . . 5 class ...
12	6, 10, 11	co 6549	. . . 4 class (0...(𝑛 − 1))
13	2	cv 1474	. . . . 5 class 𝑥
14		vk	. . . . . 6 setvar 𝑘
15	14	cv 1474	. . . . 5 class 𝑘
16	13, 15, 9	co 6549	. . . 4 class (𝑥 − 𝑘)
17	12, 16, 14	cprod 14474	. . 3 class ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘)
18	2, 3, 4, 5, 17	cmpt2 6551	. 2 class (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘))
19	1, 18	wceq 1475	1 wff FallFac = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘))

This definition is referenced by:  fallfacval  14579