Description: Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | risefaccl | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) ∈ ℂ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid | ⊢ ℂ ⊆ ℂ | |
2 | ax-1cn | ⊢ 1 ∈ ℂ | |
3 | mulcl | ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ ) | |
4 | nn0cn | ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ ) | |
5 | addcl | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐴 + 𝑘 ) ∈ ℂ ) | |
6 | 4 5 | sylan2 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 + 𝑘 ) ∈ ℂ ) |
7 | 1 2 3 6 | risefaccllem | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) ∈ ℂ ) |