Theorem fallfacval

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

	Ref	Expression
Assertion	fallfacval	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{N}}=\prod _{k=0}^{N-1}\left(A-k\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=A\to x-k=A-k$$
2	1	prodeq2sdv	$$⊢x=A\to \prod _{k=0}^{n-1}\left(x-k\right)=\prod _{k=0}^{n-1}\left(A-k\right)$$
3		oveq1	$$⊢n=N\to n-1=N-1$$
4	3	oveq2d	$$⊢n=N\to \left(0\dots n-1\right)=\left(0\dots N-1\right)$$
5	4	prodeq1d	$$⊢n=N\to \prod _{k=0}^{n-1}\left(A-k\right)=\prod _{k=0}^{N-1}\left(A-k\right)$$
6		df-fallfac	$$⊢FallFac=\left(x\in ℂ,n\in {\mathbb{N}}_0⟼\prod _{k=0}^{n-1}\left(x-k\right)\right)$$
7		prodex	$$⊢\prod _{k=0}^{N-1}\left(A-k\right)\in \mathrm{V}$$
8	2 5 6 7	ovmpo	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{N}}=\prod _{k=0}^{N-1}\left(A-k\right)$$