Metamath Proof Explorer


Theorem risefacp1d

Description: The value of the rising factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018)

Ref Expression
Hypotheses rffacp1d.1 φA
rffacp1d.2 φN0
Assertion risefacp1d φAN+1=ANA+N

Proof

Step Hyp Ref Expression
1 rffacp1d.1 φA
2 rffacp1d.2 φN0
3 risefacp1 AN0AN+1=ANA+N
4 1 2 3 syl2anc φAN+1=ANA+N