Definition df-risefac 16042

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 16041	. 2 class RiseFac
2		vx	. . 3 setvar 𝑥
3		vn	. . 3 setvar 𝑛
4		cc 11153	. . 3 class ℂ
5		cn0 12526	. . 3 class ℕ0
6		cc0 11155	. . . . 5 class 0
7	3	cv 1539	. . . . . 6 class 𝑛
8		c1 11156	. . . . . 6 class 1
9		cmin 11492	. . . . . 6 class −
10	7, 8, 9	co 7431	. . . . 5 class (𝑛 − 1)
11		cfz 13547	. . . . 5 class ...
12	6, 10, 11	co 7431	. . . 4 class (0...(𝑛 − 1))
13	2	cv 1539	. . . . 5 class 𝑥
14		vk	. . . . . 6 setvar 𝑘
15	14	cv 1539	. . . . 5 class 𝑘
16		caddc 11158	. . . . 5 class +
17	13, 15, 16	co 7431	. . . 4 class (𝑥 + 𝑘)
18	12, 17, 14	cprod 15939	. . 3 class ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 + 𝑘)
19	2, 3, 4, 5, 18	cmpo 7433	. 2 class (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 + 𝑘))
20	1, 19	wceq 1540	1 wff RiseFac = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 + 𝑘))

This definition is referenced by:  risefacval  16044