bcfallfac

Description: Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018)

		Ref	Expression
	Assertion	bcfallfac	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N^{\underline{K}}}{K!}$

Step	Hyp	Ref	Expression
1		elfz3nn0	$⊢ K \in (0 \dots N) \to N \in ℕ_{0}$
2	1	faccld	$⊢ K \in (0 \dots N) \to N! \in ℕ$
3	2	nncnd	$⊢ K \in (0 \dots N) \to N! \in ℂ$
4		fznn0sub	$⊢ K \in (0 \dots N) \to N - K \in ℕ_{0}$
5	4	faccld	$⊢ K \in (0 \dots N) \to (N - K)! \in ℕ$
6	5	nncnd	$⊢ K \in (0 \dots N) \to (N - K)! \in ℂ$
7		elfznn0	$⊢ K \in (0 \dots N) \to K \in ℕ_{0}$
8	7	faccld	$⊢ K \in (0 \dots N) \to K! \in ℕ$
9	8	nncnd	$⊢ K \in (0 \dots N) \to K! \in ℂ$
10	5	nnne0d	$⊢ K \in (0 \dots N) \to (N - K)! \neq 0$
11	8	nnne0d	$⊢ K \in (0 \dots N) \to K! \neq 0$
12	3 6 9 10 11	divdiv1d	$⊢ K \in (0 \dots N) \to \frac{\frac{N!}{(N - K)!}}{K!} = \frac{N!}{(N - K)! K!}$
13		fallfacval4	$⊢ K \in (0 \dots N) \to N^{\underline{K}} = \frac{N!}{(N - K)!}$
14	13	oveq1d	$⊢ K \in (0 \dots N) \to \frac{N^{\underline{K}}}{K!} = \frac{\frac{N!}{(N - K)!}}{K!}$
15		bcval2	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
16	12 14 15	3eqtr4rd	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N^{\underline{K}}}{K!}$

Metamath Proof Explorer