Theorem risefacfac

Description: Relate rising factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Assertion	risefacfac	$$⊢N\in {\mathbb{N}}_0\to 1^{\bar{N}}=N!$$

Proof

Step	Hyp	Ref	Expression
1		1cnd	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to 1\in ℂ$$
2		elfznn	$$⊢k\in \left(1\dots N\right)\to k\in \mathbb{N}$$
3	2	nncnd	$$⊢k\in \left(1\dots N\right)\to k\in ℂ$$
4	3	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to k\in ℂ$$
5	1 4	pncan3d	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to 1+k-1=k$$
6	5	prodeq2dv	$$⊢N\in {\mathbb{N}}_0\to \prod _{k=1}^N\left(1+k-1\right)=\prod _{k=1}^{N}k$$
7		ax-1cn	$$⊢1\in ℂ$$
8		risefacval2	$$⊢\left(1\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to 1^{\bar{N}}=\prod _{k=1}^N\left(1+k-1\right)$$
9	7 8	mpan	$$⊢N\in {\mathbb{N}}_0\to 1^{\bar{N}}=\prod _{k=1}^N\left(1+k-1\right)$$
10		fprodfac	$$⊢N\in {\mathbb{N}}_0\to N!=\prod _{k=1}^{N}k$$
11	6 9 10	3eqtr4d	$$⊢N\in {\mathbb{N}}_0\to 1^{\bar{N}}=N!$$