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=\left(x\in ℂ,n\in {\mathbb{N}}_0⟼\prod _{k=0}^{n-1}\left(x+k\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crisefac	$$classRiseFac$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		vn	$$setvarn$$
4		cn0	$$class{\mathbb{N}}_0$$
5		vk	$$setvark$$
6		cc0	$$class0$$
7		cfz	$$class\dots$$
8	3	cv	$$setvarn$$
9		cmin	$$class-$$
10		c1	$$class1$$
11	8 10 9	co	$$class\left(n-1\right)$$
12	6 11 7	co	$$class\left(0\dots n-1\right)$$
13	1	cv	$$setvarx$$
14		caddc	$$class+$$
15	5	cv	$$setvark$$
16	13 15 14	co	$$class\left(x+k\right)$$
17	12 16 5	cprod	$$class\prod _{k=0}^{n-1}\left(x+k\right)$$
18	1 3 2 4 17	cmpo	$$class\left(x\in ℂ,n\in {\mathbb{N}}_0⟼\prod _{k=0}^{n-1}\left(x+k\right)\right)$$
19	0 18	wceq	$$wffRiseFac=\left(x\in ℂ,n\in {\mathbb{N}}_0⟼\prod _{k=0}^{n-1}\left(x+k\right)\right)$$