Theorem zfallfaccl

Description: Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Assertion	zfallfaccl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		zsscn	⊢ ℤ ⊆ ℂ
2		1z	⊢ 1 ∈ ℤ
3		zmulcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
4		nn0z	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
5		zsubcl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝐴 − 𝑘 ) ∈ ℤ )
6	4 5	sylan2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 − 𝑘 ) ∈ ℤ )
7	1 2 3 6	fallfaccllem	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) ∈ ℤ )