Theorem 0fallfac

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

	Ref	Expression
Assertion	0fallfac	⊢ ( 𝑁 ∈ ℕ → ( 0 FallFac 𝑁 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		0cn	⊢ 0 ∈ ℂ
2		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
3		fallfacval	⊢ ( ( 0 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 0 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 0 − 𝑘 ) )
4	1 2 3	sylancr	⊢ ( 𝑁 ∈ ℕ → ( 0 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 0 − 𝑘 ) )
5		nnm1nn0	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
6		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
7	5 6	eleqtrdi	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
8		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℤ )
9	8	zcnd	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℂ )
10		subcl	⊢ ( ( 0 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 0 − 𝑘 ) ∈ ℂ )
11	1 9 10	sylancr	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 0 − 𝑘 ) ∈ ℂ )
12	11	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 0 − 𝑘 ) ∈ ℂ )
13		oveq2	⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = ( 0 − 0 ) )
14		0m0e0	⊢ ( 0 − 0 ) = 0
15	13 14	eqtrdi	⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = 0 )
16	7 12 15	fprod1p	⊢ ( 𝑁 ∈ ℕ → ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 0 − 𝑘 ) = ( 0 · ∏ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( 0 − 𝑘 ) ) )
17		fzfid	⊢ ( 𝑁 ∈ ℕ → ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ∈ Fin )
18		elfzelz	⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℤ )
19	18	zcnd	⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℂ )
20	1 19 10	sylancr	⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) → ( 0 − 𝑘 ) ∈ ℂ )
21	20	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 0 − 𝑘 ) ∈ ℂ )
22	17 21	fprodcl	⊢ ( 𝑁 ∈ ℕ → ∏ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( 0 − 𝑘 ) ∈ ℂ )
23	22	mul02d	⊢ ( 𝑁 ∈ ℕ → ( 0 · ∏ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( 0 − 𝑘 ) ) = 0 )
24	4 16 23	3eqtrd	⊢ ( 𝑁 ∈ ℕ → ( 0 FallFac 𝑁 ) = 0 )