Definition df-risefac 15952

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

Assertion

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

Distinct variable group:   𝑥,𝑛,𝑘

Detailed syntax breakdown of Definition df-risefac

Step	Hyp	Ref	Expression
1		crisefac 15951	. 2 class RiseFac
2		vx	. . 3 setvar 𝑥
3		vn	. . 3 setvar 𝑛
4		cc 11110	. . 3 class ℂ
5		cn0 12474	. . 3 class ℕ0
6		cc0 11112	. . . . 5 class 0
7	3	cv 1540	. . . . . 6 class 𝑛
8		c1 11113	. . . . . 6 class 1
9		cmin 11446	. . . . . 6 class −
10	7, 8, 9	co 7411	. . . . 5 class (𝑛 − 1)
11		cfz 13486	. . . . 5 class ...
12	6, 10, 11	co 7411	. . . 4 class (0...(𝑛 − 1))
13	2	cv 1540	. . . . 5 class 𝑥
14		vk	. . . . . 6 setvar 𝑘
15	14	cv 1540	. . . . 5 class 𝑘
16		caddc 11115	. . . . 5 class +
17	13, 15, 16	co 7411	. . . 4 class (𝑥 + 𝑘)
18	12, 17, 14	cprod 15851	. . 3 class ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 + 𝑘)
19	2, 3, 4, 5, 18	cmpo 7413	. 2 class (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 + 𝑘))
20	1, 19	wceq 1541	1 wff RiseFac = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 + 𝑘))

This definition is referenced by:  risefacval  15954