bcval

Description: Value of the binomial coefficient, N choose K . Definition of binomial coefficient in Gleason p. 295. As suggested by Gleason, we define it to be 0 when 0 <_ K <_ N does not hold. See bcval2 for the value in the standard domain. (Contributed by NM, 10-Jul-2005) (Revised by Mario Carneiro, 7-Nov-2013)

		Ref	Expression
	Assertion	bcval	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) = if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ n = N \to (0 \dots n) = (0 \dots N)$
2	1	eleq2d	$⊢ n = N \to (k \in (0 \dots n) \leftrightarrow k \in (0 \dots N))$
3		fveq2	$⊢ n = N \to n! = N!$
4		fvoveq1	$⊢ n = N \to (n - k)! = (N - k)!$
5	4	oveq1d	$⊢ n = N \to (n - k)! k! = (N - k)! k!$
6	3 5	oveq12d	$⊢ n = N \to \frac{n!}{(n - k)! k!} = \frac{N!}{(N - k)! k!}$
7	2 6	ifbieq1d	$⊢ n = N \to if (k \in (0 \dots n), \frac{n!}{(n - k)! k!}, 0) = if (k \in (0 \dots N), \frac{N!}{(N - k)! k!}, 0)$
8		eleq1	$⊢ k = K \to (k \in (0 \dots N) \leftrightarrow K \in (0 \dots N))$
9		oveq2	$⊢ k = K \to N - k = N - K$
10	9	fveq2d	$⊢ k = K \to (N - k)! = (N - K)!$
11		fveq2	$⊢ k = K \to k! = K!$
12	10 11	oveq12d	$⊢ k = K \to (N - k)! k! = (N - K)! K!$
13	12	oveq2d	$⊢ k = K \to \frac{N!}{(N - k)! k!} = \frac{N!}{(N - K)! K!}$
14	8 13	ifbieq1d	$⊢ k = K \to if (k \in (0 \dots N), \frac{N!}{(N - k)! k!}, 0) = if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0)$
15		df-bc	$⊢ (\binom{.}{.}) = (n \in ℕ_{0}, k \in ℤ ⟼ if (k \in (0 \dots n), \frac{n!}{(n - k)! k!}, 0))$
16		ovex	$⊢ \frac{N!}{(N - K)! K!} \in V$
17		c0ex	$⊢ 0 \in V$
18	16 17	ifex	$⊢ if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0) \in V$
19	7 14 15 18	ovmpo	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) = if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0)$

Metamath Proof Explorer

Theorem bcval

Proof