Metamath Proof Explorer


Theorem fallfacp1d

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

Ref Expression
Hypotheses rffacp1d.1 ( 𝜑𝐴 ∈ ℂ )
rffacp1d.2 ( 𝜑𝑁 ∈ ℕ0 )
Assertion fallfacp1d ( 𝜑 → ( 𝐴 FallFac ( 𝑁 + 1 ) ) = ( ( 𝐴 FallFac 𝑁 ) · ( 𝐴𝑁 ) ) )

Proof

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