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 ) ) ( 𝐴 − 𝑘 ) )