Metamath Proof Explorer


Theorem refallfaccl

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

Ref Expression
Assertion refallfaccl ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 ax-resscn ℝ ⊆ ℂ
2 1re 1 ∈ ℝ
3 remulcl ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
4 nn0re ( 𝑘 ∈ ℕ0𝑘 ∈ ℝ )
5 resubcl ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐴𝑘 ) ∈ ℝ )
6 4 5 sylan2 ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℝ )
7 1 2 3 6 fallfaccllem ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) ∈ ℝ )