Definition df-risefac

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crisefac	⊢ RiseFac
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		vn	⊢ 𝑛
4		cn0	⊢ ℕ0
5		vk	⊢ 𝑘
6		cc0	⊢ 0
7		cfz	⊢ ...
8	3	cv	⊢ 𝑛
9		cmin	⊢ −
10		c1	⊢ 1
11	8 10 9	co	⊢ ( 𝑛 − 1 )
12	6 11 7	co	⊢ ( 0 ... ( 𝑛 − 1 ) )
13	1	cv	⊢ 𝑥
14		caddc	⊢ +
15	5	cv	⊢ 𝑘
16	13 15 14	co	⊢ ( 𝑥 + 𝑘 )
17	12 16 5	cprod	⊢ ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 + 𝑘 )
18	1 3 2 4 17	cmpo	⊢ ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 + 𝑘 ) )
19	0 18	wceq	⊢ RiseFac = ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 + 𝑘 ) )