Description: Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | nnrisefaccl | ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) ∈ ℕ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnsscn | ⊢ ℕ ⊆ ℂ | |
2 | 1nn | ⊢ 1 ∈ ℕ | |
3 | nnmulcl | ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 · 𝑦 ) ∈ ℕ ) | |
4 | nnnn0addcl | ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 + 𝑘 ) ∈ ℕ ) | |
5 | 1 2 3 4 | risefaccllem | ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) ∈ ℕ ) |