fallfacval3

Description: A product representation of falling factorial when A is a nonnegative integer. (Contributed by Scott Fenton, 20-Mar-2018)

		Ref	Expression
	Assertion	fallfacval3	$⊢ N \in (0 \dots A) \to A^{\underline{N}} = \prod_{k = A - (N - 1)}^{A} k$

Proof

Step	Hyp	Ref	Expression
1		elfz3nn0	$⊢ N \in (0 \dots A) \to A \in ℕ_{0}$
2	1	nn0cnd	$⊢ N \in (0 \dots A) \to A \in ℂ$
3		elfznn0	$⊢ N \in (0 \dots A) \to N \in ℕ_{0}$
4		fallfacval	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\underline{N}} = \prod_{j = 0}^{N - 1} (A - j)$
5	2 3 4	syl2anc	$⊢ N \in (0 \dots A) \to A^{\underline{N}} = \prod_{j = 0}^{N - 1} (A - j)$
6		elfzel2	$⊢ N \in (0 \dots A) \to A \in ℤ$
7		elfzel1	$⊢ N \in (0 \dots A) \to 0 \in ℤ$
8		elfzelz	$⊢ N \in (0 \dots A) \to N \in ℤ$
9		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
10	8 9	syl	$⊢ N \in (0 \dots A) \to N - 1 \in ℤ$
11		elfzelz	$⊢ j \in (0 \dots N - 1) \to j \in ℤ$
12	11	zcnd	$⊢ j \in (0 \dots N - 1) \to j \in ℂ$
13		subcl	$⊢ (A \in ℂ \land j \in ℂ) \to A - j \in ℂ$
14	2 12 13	syl2an	$⊢ (N \in (0 \dots A) \land j \in (0 \dots N - 1)) \to A - j \in ℂ$
15		oveq2	$⊢ j = A - k \to A - j = A - (A - k)$
16	6 7 10 14 15	fprodrev	$⊢ N \in (0 \dots A) \to \prod_{j = 0}^{N - 1} (A - j) = \prod_{k = A - (N - 1)}^{A - 0} (A - (A - k))$
17	2	subid1d	$⊢ N \in (0 \dots A) \to A - 0 = A$
18	17	oveq2d	$⊢ N \in (0 \dots A) \to (A - (N - 1) \dots A - 0) = (A - (N - 1) \dots A)$
19	2	adantr	$⊢ (N \in (0 \dots A) \land k \in (A - (N - 1) \dots A - 0)) \to A \in ℂ$
20		elfzelz	$⊢ k \in (A - (N - 1) \dots A - 0) \to k \in ℤ$
21	20	zcnd	$⊢ k \in (A - (N - 1) \dots A - 0) \to k \in ℂ$
22	21	adantl	$⊢ (N \in (0 \dots A) \land k \in (A - (N - 1) \dots A - 0)) \to k \in ℂ$
23	19 22	nncand	$⊢ (N \in (0 \dots A) \land k \in (A - (N - 1) \dots A - 0)) \to A - (A - k) = k$
24	18 23	prodeq12dv	$⊢ N \in (0 \dots A) \to \prod_{k = A - (N - 1)}^{A - 0} (A - (A - k)) = \prod_{k = A - (N - 1)}^{A} k$
25	5 16 24	3eqtrd	$⊢ N \in (0 \dots A) \to A^{\underline{N}} = \prod_{k = A - (N - 1)}^{A} k$

Metamath Proof Explorer

Theorem fallfacval3

Proof