Metamath Proof Explorer


Theorem risefaccl

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

Ref Expression
Assertion risefaccl ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) ∈ ℂ )

Proof

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 𝑁 ) ∈ ℂ )