fallfacval4

Description: Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018)

		Ref	Expression
	Assertion	fallfacval4	$⊢ N \in (0 \dots A) \to A^{\underline{N}} = \frac{A!}{(A - N)!}$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ N \in (0 \dots A) \to (A - N + 1 \dots A) \in Fin$
2		elfzelz	$⊢ k \in (A - N + 1 \dots A) \to k \in ℤ$
3	2	zcnd	$⊢ k \in (A - N + 1 \dots A) \to k \in ℂ$
4	3	adantl	$⊢ (N \in (0 \dots A) \land k \in (A - N + 1 \dots A)) \to k \in ℂ$
5	1 4	fprodcl	$⊢ N \in (0 \dots A) \to \prod_{k = A - N + 1}^{A} k \in ℂ$
6		fzfid	$⊢ N \in (0 \dots A) \to (1 \dots A - N) \in Fin$
7		elfznn	$⊢ k \in (1 \dots A - N) \to k \in ℕ$
8	7	adantl	$⊢ (N \in (0 \dots A) \land k \in (1 \dots A - N)) \to k \in ℕ$
9	8	nncnd	$⊢ (N \in (0 \dots A) \land k \in (1 \dots A - N)) \to k \in ℂ$
10	6 9	fprodcl	$⊢ N \in (0 \dots A) \to \prod_{k = 1}^{A - N} k \in ℂ$
11	8	nnne0d	$⊢ (N \in (0 \dots A) \land k \in (1 \dots A - N)) \to k \neq 0$
12	6 9 11	fprodn0	$⊢ N \in (0 \dots A) \to \prod_{k = 1}^{A - N} k \neq 0$
13	5 10 12	divcan3d	$⊢ N \in (0 \dots A) \to \frac{\prod_{k = 1}^{A - N} k \prod_{k = A - N + 1}^{A} k}{\prod_{k = 1}^{A - N} k} = \prod_{k = A - N + 1}^{A} k$
14		fznn0sub	$⊢ N \in (0 \dots A) \to A - N \in ℕ_{0}$
15	14	nn0red	$⊢ N \in (0 \dots A) \to A - N \in ℝ$
16	15	ltp1d	$⊢ N \in (0 \dots A) \to A - N < A - N + 1$
17		fzdisj	$⊢ A - N < A - N + 1 \to (1 \dots A - N) \cap (A - N + 1 \dots A) = \emptyset$
18	16 17	syl	$⊢ N \in (0 \dots A) \to (1 \dots A - N) \cap (A - N + 1 \dots A) = \emptyset$
19		nn0p1nn	$⊢ A - N \in ℕ_{0} \to A - N + 1 \in ℕ$
20	14 19	syl	$⊢ N \in (0 \dots A) \to A - N + 1 \in ℕ$
21		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
22	20 21	eleqtrdi	$⊢ N \in (0 \dots A) \to A - N + 1 \in ℤ_{\geq 1}$
23	14	nn0zd	$⊢ N \in (0 \dots A) \to A - N \in ℤ$
24		elfzel2	$⊢ N \in (0 \dots A) \to A \in ℤ$
25		elfzle1	$⊢ N \in (0 \dots A) \to 0 \leq N$
26	24	zred	$⊢ N \in (0 \dots A) \to A \in ℝ$
27		elfzelz	$⊢ N \in (0 \dots A) \to N \in ℤ$
28	27	zred	$⊢ N \in (0 \dots A) \to N \in ℝ$
29	26 28	subge02d	$⊢ N \in (0 \dots A) \to (0 \leq N \leftrightarrow A - N \leq A)$
30	25 29	mpbid	$⊢ N \in (0 \dots A) \to A - N \leq A$
31		eluz2	$⊢ A \in ℤ_{\geq (A - N)} \leftrightarrow (A - N \in ℤ \land A \in ℤ \land A - N \leq A)$
32	23 24 30 31	syl3anbrc	$⊢ N \in (0 \dots A) \to A \in ℤ_{\geq (A - N)}$
33		fzsplit2	$⊢ (A - N + 1 \in ℤ_{\geq 1} \land A \in ℤ_{\geq (A - N)}) \to (1 \dots A) = (1 \dots A - N) \cup (A - N + 1 \dots A)$
34	22 32 33	syl2anc	$⊢ N \in (0 \dots A) \to (1 \dots A) = (1 \dots A - N) \cup (A - N + 1 \dots A)$
35		fzfid	$⊢ N \in (0 \dots A) \to (1 \dots A) \in Fin$
36		elfznn	$⊢ k \in (1 \dots A) \to k \in ℕ$
37	36	nncnd	$⊢ k \in (1 \dots A) \to k \in ℂ$
38	37	adantl	$⊢ (N \in (0 \dots A) \land k \in (1 \dots A)) \to k \in ℂ$
39	18 34 35 38	fprodsplit	$⊢ N \in (0 \dots A) \to \prod_{k = 1}^{A} k = \prod_{k = 1}^{A - N} k \prod_{k = A - N + 1}^{A} k$
40	39	oveq1d	$⊢ N \in (0 \dots A) \to \frac{\prod_{k = 1}^{A} k}{\prod_{k = 1}^{A - N} k} = \frac{\prod_{k = 1}^{A - N} k \prod_{k = A - N + 1}^{A} k}{\prod_{k = 1}^{A - N} k}$
41	24	zcnd	$⊢ N \in (0 \dots A) \to A \in ℂ$
42	27	zcnd	$⊢ N \in (0 \dots A) \to N \in ℂ$
43		1cnd	$⊢ N \in (0 \dots A) \to 1 \in ℂ$
44	41 42 43	subsubd	$⊢ N \in (0 \dots A) \to A - (N - 1) = A - N + 1$
45	44	oveq1d	$⊢ N \in (0 \dots A) \to (A - (N - 1) \dots A) = (A - N + 1 \dots A)$
46	45	prodeq1d	$⊢ N \in (0 \dots A) \to \prod_{k = A - (N - 1)}^{A} k = \prod_{k = A - N + 1}^{A} k$
47	13 40 46	3eqtr4rd	$⊢ N \in (0 \dots A) \to \prod_{k = A - (N - 1)}^{A} k = \frac{\prod_{k = 1}^{A} k}{\prod_{k = 1}^{A - N} k}$
48		fallfacval3	$⊢ N \in (0 \dots A) \to A^{\underline{N}} = \prod_{k = A - (N - 1)}^{A} k$
49		elfz3nn0	$⊢ N \in (0 \dots A) \to A \in ℕ_{0}$
50		fprodfac	$⊢ A \in ℕ_{0} \to A! = \prod_{k = 1}^{A} k$
51	49 50	syl	$⊢ N \in (0 \dots A) \to A! = \prod_{k = 1}^{A} k$
52		fprodfac	$⊢ A - N \in ℕ_{0} \to (A - N)! = \prod_{k = 1}^{A - N} k$
53	14 52	syl	$⊢ N \in (0 \dots A) \to (A - N)! = \prod_{k = 1}^{A - N} k$
54	51 53	oveq12d	$⊢ N \in (0 \dots A) \to \frac{A!}{(A - N)!} = \frac{\prod_{k = 1}^{A} k}{\prod_{k = 1}^{A - N} k}$
55	47 48 54	3eqtr4d	$⊢ N \in (0 \dots A) \to A^{\underline{N}} = \frac{A!}{(A - N)!}$

Metamath Proof Explorer

Theorem fallfacval4

Proof