This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )