This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
rffacp1d.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion risefacp1d ( 𝜑 → ( 𝐴 RiseFac ( 𝑁 + 1 ) ) = ( ( 𝐴 RiseFac 𝑁 ) · ( 𝐴 + 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 rffacp1d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 rffacp1d.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3 risefacp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac ( 𝑁 + 1 ) ) = ( ( 𝐴 RiseFac 𝑁 ) · ( 𝐴 + 𝑁 ) ) )
4 1 2 3 syl2anc ⊢ ( 𝜑 → ( 𝐴 RiseFac ( 𝑁 + 1 ) ) = ( ( 𝐴 RiseFac 𝑁 ) · ( 𝐴 + 𝑁 ) ) )