Metamath Proof Explorer

Theorem bc0k

Description: The binomial coefficient " 0 choose K " is 0 for a positive integer K. Note that ( 0 _C 0 ) = 1 (see bcn0 ). (Contributed by Alexander van der Vekens, 1-Jan-2018)

		Ref	Expression
	Assertion	bc0k	$⊢ K \in ℕ \to (\binom{0}{K}) = 0$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2		nnz	$⊢ K \in ℕ \to K \in ℤ$
3		nngt0	$⊢ K \in ℕ \to 0 < K$
4	3	olcd	$⊢ K \in ℕ \to (K < 0 \lor 0 < K)$
5		bcval4	$⊢ (0 \in ℕ_{0} \land K \in ℤ \land (K < 0 \lor 0 < K)) \to (\binom{0}{K}) = 0$
6	1 2 4 5	mp3an2i	$⊢ K \in ℕ \to (\binom{0}{K}) = 0$