bcval2

Description: Value of the binomial coefficient, N choose K , in its standard domain. (Contributed by NM, 9-Jun-2005) (Revised by Mario Carneiro, 7-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		elfz3nn0	$⊢ K \in (0 \dots N) \to N \in ℕ_{0}$
2		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
3		bcval	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) = if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0)$
4	1 2 3	syl2anc	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0)$
5		iftrue	$⊢ K \in (0 \dots N) \to if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0) = \frac{N!}{(N - K)! K!}$
6	4 5	eqtrd	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$

Metamath Proof Explorer

Theorem bcval2

Proof