Theorem risefac0

Description: The value of the rising factorial when N = 0 . (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Assertion	risefac0	$$⊢A\in ℂ\to A^{\bar{0}}=1$$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$$⊢0\in {\mathbb{N}}_0$$
2		risefacval	$$⊢\left(A\in ℂ\wedge 0\in {\mathbb{N}}_0\right)\to A^{\bar{0}}=\prod _{k=0}^{0-1}\left(A+k\right)$$
3	1 2	mpan2	$$⊢A\in ℂ\to A^{\bar{0}}=\prod _{k=0}^{0-1}\left(A+k\right)$$
4		fz00m1	$$⊢\left(0\dots 0-1\right)=\varnothing$$
5	4	prodeq1i	$$⊢\prod _{k=0}^{0-1}\left(A+k\right)=\prod _{k\in \varnothing }\left(A+k\right)$$
6		prod0	$$⊢\prod _{k\in \varnothing }\left(A+k\right)=1$$
7	5 6	eqtri	$$⊢\prod _{k=0}^{0-1}\left(A+k\right)=1$$
8	3 7	eqtrdi	$$⊢A\in ℂ\to A^{\bar{0}}=1$$