fallfacval

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

		Ref	Expression
	Assertion	fallfacval	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\underline{N}} = \prod_{k = 0}^{N - 1} (A - k)$

Step	Hyp	Ref	Expression
1		oveq1	$⊢ x = A \to x - k = A - k$
2	1	prodeq2sdv	$⊢ x = A \to \prod_{k = 0}^{n - 1} (x - k) = \prod_{k = 0}^{n - 1} (A - k)$
3		oveq1	$⊢ n = N \to n - 1 = N - 1$
4	3	oveq2d	$⊢ n = N \to (0 \dots n - 1) = (0 \dots N - 1)$
5	4	prodeq1d	$⊢ n = N \to \prod_{k = 0}^{n - 1} (A - k) = \prod_{k = 0}^{N - 1} (A - k)$
6		df-fallfac	$⊢ FallFac = (x \in ℂ, n \in ℕ_{0} ⟼ \prod_{k = 0}^{n - 1} (x - k))$
7		prodex	$⊢ \prod_{k = 0}^{N - 1} (A - k) \in V$
8	2 5 6 7	ovmpo	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\underline{N}} = \prod_{k = 0}^{N - 1} (A - k)$

Metamath Proof Explorer