Metamath Proof Explorer


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