Database
REAL AND COMPLEX NUMBERS
Elementary limits and convergence
Falling and Rising Factorial
nnrisefaccl
Next ⟩
zrisefaccl
Metamath Proof Explorer
Ascii
Unicode
Theorem
nnrisefaccl
Description:
Closure law for rising factorial.
(Contributed by
Scott Fenton
, 5-Jan-2018)
Ref
Expression
Assertion
nnrisefaccl
⊢
A
∈
ℕ
∧
N
∈
ℕ
0
→
A
N
‾
∈
ℕ
Proof
Step
Hyp
Ref
Expression
1
nnsscn
⊢
ℕ
⊆
ℂ
2
1nn
⊢
1
∈
ℕ
3
nnmulcl
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
x
⁢
y
∈
ℕ
4
nnnn0addcl
⊢
A
∈
ℕ
∧
k
∈
ℕ
0
→
A
+
k
∈
ℕ
5
1
2
3
4
risefaccllem
⊢
A
∈
ℕ
∧
N
∈
ℕ
0
→
A
N
‾
∈
ℕ