fallfacp1

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

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

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
2	1	adantl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N \in ℂ$
3		1cnd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to 1 \in ℂ$
4	2 3	pncand	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N + 1 - 1 = N$
5	4	oveq2d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (0 \dots N + 1 - 1) = (0 \dots N)$
6	5	prodeq1d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \prod_{k = 0}^{N + 1 - 1} (A - k) = \prod_{k = 0}^{N} (A - k)$
7		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
8	7	bilani	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N \in ℤ_{\geq 0}$
9		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
10	9	nn0cnd	$⊢ k \in (0 \dots N) \to k \in ℂ$
11		subcl	$⊢ (A \in ℂ \land k \in ℂ) \to A - k \in ℂ$
12	10 11	sylan2	$⊢ (A \in ℂ \land k \in (0 \dots N)) \to A - k \in ℂ$
13	12	adantlr	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to A - k \in ℂ$
14		oveq2	$⊢ k = N \to A - k = A - N$
15	8 13 14	fprodm1	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \prod_{k = 0}^{N} (A - k) = \prod_{k = 0}^{N - 1} (A - k) (A - N)$
16	6 15	eqtrd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \prod_{k = 0}^{N + 1 - 1} (A - k) = \prod_{k = 0}^{N - 1} (A - k) (A - N)$
17		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
18		fallfacval	$⊢ (A \in ℂ \land N + 1 \in ℕ_{0}) \to A^{\underline{(N + 1)}} = \prod_{k = 0}^{N + 1 - 1} (A - k)$
19	17 18	sylan2	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\underline{(N + 1)}} = \prod_{k = 0}^{N + 1 - 1} (A - k)$
20		fallfacval	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\underline{N}} = \prod_{k = 0}^{N - 1} (A - k)$
21	20	oveq1d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (A^{\underline{N}}) (A - N) = \prod_{k = 0}^{N - 1} (A - k) (A - N)$
22	16 19 21	3eqtr4d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\underline{(N + 1)}} = (A^{\underline{N}}) (A - N)$

Metamath Proof Explorer

Theorem fallfacp1

Proof