Metamath Proof Explorer


Theorem rerisefaccl

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

Ref Expression
Assertion rerisefaccl A N 0 A N

Proof

Step Hyp Ref Expression
1 ax-resscn
2 1re 1
3 remulcl x y x y
4 nn0re k 0 k
5 readdcl A k A + k
6 4 5 sylan2 A k 0 A + k
7 1 2 3 6 risefaccllem A N 0 A N