This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bcval3

Description: Value of the binomial coefficient, N choose K , outside of its standard domain. Remark in Gleason p. 295. (Contributed by NM, 14-Jul-2005) (Revised by Mario Carneiro, 8-Nov-2013)

		Ref	Expression
	Assertion	bcval3	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$

Proof

Step	Hyp	Ref	Expression
1		bcval	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) = if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0)$
2	1	3adant3	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0)$
3		iffalse	$⊢ \neg K \in (0 \dots N) \to if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0) = 0$
4	3	3ad2ant3	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to if (K \in (0 \dots N), \frac{N!}{(N - K)! K!}, 0) = 0$
5	2 4	eqtrd	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$