fallfacval2

Description: One-based value of falling factorial. (Contributed by Scott Fenton, 15-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		fallfacval	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\underline{N}} = \prod_{n = 0}^{N - 1} (A - n)$
2		1zzd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to 1 \in ℤ$
3		0zd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to 0 \in ℤ$
4		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
5		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
6	4 5	syl	$⊢ N \in ℕ_{0} \to N - 1 \in ℤ$
7	6	adantl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N - 1 \in ℤ$
8		simpl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A \in ℂ$
9		elfznn0	$⊢ n \in (0 \dots N - 1) \to n \in ℕ_{0}$
10	9	nn0cnd	$⊢ n \in (0 \dots N - 1) \to n \in ℂ$
11		subcl	$⊢ (A \in ℂ \land n \in ℂ) \to A - n \in ℂ$
12	8 10 11	syl2an	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land n \in (0 \dots N - 1)) \to A - n \in ℂ$
13		oveq2	$⊢ n = k - 1 \to A - n = A - (k - 1)$
14	2 3 7 12 13	fprodshft	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \prod_{n = 0}^{N - 1} (A - n) = \prod_{k = 0 + 1}^{N - 1 + 1} (A - (k - 1))$
15		0p1e1	$⊢ 0 + 1 = 1$
16	15	a1i	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to 0 + 1 = 1$
17		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
18		1cnd	$⊢ N \in ℕ_{0} \to 1 \in ℂ$
19	17 18	npcand	$⊢ N \in ℕ_{0} \to N - 1 + 1 = N$
20	19	adantl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N - 1 + 1 = N$
21	16 20	oveq12d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (0 + 1 \dots N - 1 + 1) = (1 \dots N)$
22	21	prodeq1d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \prod_{k = 0 + 1}^{N - 1 + 1} (A - (k - 1)) = \prod_{k = 1}^{N} (A - (k - 1))$
23	1 14 22	3eqtrd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\underline{N}} = \prod_{k = 1}^{N} (A - (k - 1))$

Metamath Proof Explorer

Theorem fallfacval2

Proof