Theorem fallfacfac

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

	Ref	Expression
Assertion	fallfacfac	$$⊢N\in {\mathbb{N}}_0\to N^{\underset{\_}{N}}=N!$$

Proof

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