fallfacfac

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

		Ref	Expression
	Assertion	fallfacfac	$⊢ N \in ℕ_{0} \to N^{\underline{N}} = N!$

Step	Hyp	Ref	Expression
1		nn0fz0	$⊢ N \in ℕ_{0} \leftrightarrow N \in (0 \dots N)$
2		fallfacval4	$⊢ N \in (0 \dots N) \to N^{\underline{N}} = \frac{N!}{(N - N)!}$
3	1 2	sylbi	$⊢ N \in ℕ_{0} \to N^{\underline{N}} = \frac{N!}{(N - N)!}$
4		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
5	4	subidd	$⊢ N \in ℕ_{0} \to N - N = 0$
6	5	fveq2d	$⊢ N \in ℕ_{0} \to (N - N)! = 0!$
7		fac0	$⊢ 0! = 1$
8	6 7	eqtrdi	$⊢ N \in ℕ_{0} \to (N - N)! = 1$
9	8	oveq2d	$⊢ N \in ℕ_{0} \to \frac{N!}{(N - N)!} = \frac{N!}{1}$
10		faccl	$⊢ N \in ℕ_{0} \to N! \in ℕ$
11	10	nncnd	$⊢ N \in ℕ_{0} \to N! \in ℂ$
12	11	div1d	$⊢ N \in ℕ_{0} \to \frac{N!}{1} = N!$
13	3 9 12	3eqtrd	$⊢ N \in ℕ_{0} \to N^{\underline{N}} = N!$

Metamath Proof Explorer