Theorem 0fallfac

Description: The value of the zero falling factorial at natural N . (Contributed by Scott Fenton, 17-Feb-2018)

	Ref	Expression
Assertion	0fallfac	$$⊢N\in \mathbb{N}\to 0^{\underset{\_}{N}}=0$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
3		fallfacval	$$⊢\left(0\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to 0^{\underset{\_}{N}}=\prod _{k=0}^{N-1}\left(0-k\right)$$
4	1 2 3	sylancr	$$⊢N\in \mathbb{N}\to 0^{\underset{\_}{N}}=\prod _{k=0}^{N-1}\left(0-k\right)$$
5		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
6		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
7	5 6	eleqtrdi	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{Z}}_{\ge 0}$$
8		elfzelz	$$⊢k\in \left(0\dots N-1\right)\to k\in \mathbb{Z}$$
9	8	zcnd	$$⊢k\in \left(0\dots N-1\right)\to k\in ℂ$$
10		subcl	$$⊢\left(0\in ℂ\wedge k\in ℂ\right)\to 0-k\in ℂ$$
11	1 9 10	sylancr	$$⊢k\in \left(0\dots N-1\right)\to 0-k\in ℂ$$
12	11	adantl	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(0\dots N-1\right)\right)\to 0-k\in ℂ$$
13		oveq2	$$⊢k=0\to 0-k=0-0$$
14		0m0e0	$$⊢0-0=0$$
15	13 14	eqtrdi	$$⊢k=0\to 0-k=0$$
16	7 12 15	fprod1p	$$⊢N\in \mathbb{N}\to \prod _{k=0}^{N-1}\left(0-k\right)=0\cdot \prod _{k=0+1}^{N-1}\left(0-k\right)$$
17		fzfid	$$⊢N\in \mathbb{N}\to \left(0+1\dots N-1\right)\in \mathrm{Fin}$$
18		elfzelz	$$⊢k\in \left(0+1\dots N-1\right)\to k\in \mathbb{Z}$$
19	18	zcnd	$$⊢k\in \left(0+1\dots N-1\right)\to k\in ℂ$$
20	1 19 10	sylancr	$$⊢k\in \left(0+1\dots N-1\right)\to 0-k\in ℂ$$
21	20	adantl	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(0+1\dots N-1\right)\right)\to 0-k\in ℂ$$
22	17 21	fprodcl	$$⊢N\in \mathbb{N}\to \prod _{k=0+1}^{N-1}\left(0-k\right)\in ℂ$$
23	22	mul02d	$$⊢N\in \mathbb{N}\to 0\cdot \prod _{k=0+1}^{N-1}\left(0-k\right)=0$$
24	4 16 23	3eqtrd	$$⊢N\in \mathbb{N}\to 0^{\underset{\_}{N}}=0$$