Metamath Proof Explorer


Theorem fallfacval

Description: The value of the falling factorial function. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion fallfacval ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴𝑘 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ( 𝑥 = 𝐴 → ( 𝑥𝑘 ) = ( 𝐴𝑘 ) )
2 1 prodeq2sdv ( 𝑥 = 𝐴 → ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥𝑘 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴𝑘 ) )
3 oveq1 ( 𝑛 = 𝑁 → ( 𝑛 − 1 ) = ( 𝑁 − 1 ) )
4 3 oveq2d ( 𝑛 = 𝑁 → ( 0 ... ( 𝑛 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) ) )
5 4 prodeq1d ( 𝑛 = 𝑁 → ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴𝑘 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴𝑘 ) )
6 df-fallfac FallFac = ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥𝑘 ) )
7 prodex 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴𝑘 ) ∈ V
8 2 5 6 7 ovmpo ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴𝑘 ) )