Definition df-risefac 14071

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.)

Assertion

Ref	Expression
df-risefac	|- RiseFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k ) )

Distinct variable group:   x, n, k

Detailed syntax breakdown of Definition df-risefac

Step	Hyp	Ref	Expression
1		crisefac 14070	. 2 class RiseFac
2		vx	. . 3 setvar x
3		vn	. . 3 setvar n
4		cc 9542	. . 3 class CC
5		cn0 10876	. . 3 class NN0
6		cc0 9544	. . . . 5 class 0
7	3	cv 1445	. . . . . 6 class n
8		c1 9545	. . . . . 6 class 1
9		cmin 9865	. . . . . 6 class -
10	7, 8, 9	co 6295	. . . . 5 class ( n - 1 )
11		cfz 11791	. . . . 5 class ...
12	6, 10, 11	co 6295	. . . 4 class ( 0 ... ( n - 1 ) )
13	2	cv 1445	. . . . 5 class x
14		vk	. . . . . 6 setvar k
15	14	cv 1445	. . . . 5 class k
16		caddc 9547	. . . . 5 class +
17	13, 15, 16	co 6295	. . . 4 class ( x + k )
18	12, 17, 14	cprod 13971	. . 3 class prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k )
19	2, 3, 4, 5, 18	cmpt2 6297	. 2 class ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k ) )
20	1, 19	wceq 1446	1 wff RiseFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k ) )

This definition is referenced by:  risefacval  14073