risefacfac

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

		Ref	Expression
	Assertion	risefacfac	$⊢ N \in ℕ_{0} \to 1^{\overline{N}} = N!$

Step	Hyp	Ref	Expression
1		1cnd	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to 1 \in ℂ$
2		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
3	2	nncnd	$⊢ k \in (1 \dots N) \to k \in ℂ$
4	3	adantl	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to k \in ℂ$
5	1 4	pncan3d	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to 1 + k - 1 = k$
6	5	prodeq2dv	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N} (1 + k - 1) = \prod_{k = 1}^{N} k$
7		ax-1cn	$⊢ 1 \in ℂ$
8		risefacval2	$⊢ (1 \in ℂ \land N \in ℕ_{0}) \to 1^{\overline{N}} = \prod_{k = 1}^{N} (1 + k - 1)$
9	7 8	mpan	$⊢ N \in ℕ_{0} \to 1^{\overline{N}} = \prod_{k = 1}^{N} (1 + k - 1)$
10		fprodfac	$⊢ N \in ℕ_{0} \to N! = \prod_{k = 1}^{N} k$
11	6 9 10	3eqtr4d	$⊢ N \in ℕ_{0} \to 1^{\overline{N}} = N!$

Metamath Proof Explorer