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 = (x \in ℂ, n \in ℕ_{0} ⟼ \prod_{k = 0}^{n - 1} (x + k))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crisefac	$class RiseFac$
1		vx	$setvar x$
2		cc	$class ℂ$
3		vn	$setvar n$
4		cn0	$class ℕ_{0}$
5		vk	$setvar k$
6		cc0	$class 0$
7		cfz	$class \dots$
8	3	cv	$setvar n$
9		cmin	$class -$
10		c1	$class 1$
11	8 10 9	co	$class (n - 1)$
12	6 11 7	co	$class (0 \dots n - 1)$
13	1	cv	$setvar x$
14		caddc	$class +$
15	5	cv	$setvar k$
16	13 15 14	co	$class (x + k)$
17	12 16 5	cprod	$class \prod_{k = 0}^{n - 1} (x + k)$
18	1 3 2 4 17	cmpo	$class (x \in ℂ, n \in ℕ_{0} ⟼ \prod_{k = 0}^{n - 1} (x + k))$
19	0 18	wceq	$wff RiseFac = (x \in ℂ, n \in ℕ_{0} ⟼ \prod_{k = 0}^{n - 1} (x + k))$

Metamath Proof Explorer

Definition df-risefac

Detailed syntax breakdown