Definition df-risefac 25275

Description: Define the rising factorial function. This is the function ( A x. ( A + 1 ) x. ... ( A + N ) ) for complex A and non-negative 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 25274	. 2 class RiseFac
2		vx	. . 3 set x
3		vn	. . 3 set n
4		cc 8944	. . 3 class CC
5		cn0 10177	. . 3 class NN0
6		cc0 8946	. . . . 5 class 0
7	3	cv 1648	. . . . . 6 class n
8		c1 8947	. . . . . 6 class 1
9		cmin 9247	. . . . . 6 class -
10	7, 8, 9	co 6040	. . . . 5 class ( n - 1 )
11		cfz 10999	. . . . 5 class ...
12	6, 10, 11	co 6040	. . . 4 class ( 0 ... ( n - 1 ) )
13	2	cv 1648	. . . . 5 class x
14		vk	. . . . . 6 set k
15	14	cv 1648	. . . . 5 class k
16		caddc 8949	. . . . 5 class +
17	13, 15, 16	co 6040	. . . 4 class ( x + k )
18	12, 17, 14	cprod 25184	. . 3 class prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k )
19	2, 3, 4, 5, 18	cmpt2 6042	. 2 class ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k ) )
20	1, 19	wceq 1649	1 wff RiseFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k ) )

This definition is referenced by:  risefacval  25277