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	⊢ ( 𝐾 ∈ ℕ → ( 0 C 𝐾 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		0nn0	⊢ 0 ∈ ℕ0
2		nnz	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
3		nngt0	⊢ ( 𝐾 ∈ ℕ → 0 < 𝐾 )
4	3	olcd	⊢ ( 𝐾 ∈ ℕ → ( 𝐾 < 0 ∨ 0 < 𝐾 ) )
5		bcval4	⊢ ( ( 0 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ( 𝐾 < 0 ∨ 0 < 𝐾 ) ) → ( 0 C 𝐾 ) = 0 )
6	1 2 4 5	mp3an2i	⊢ ( 𝐾 ∈ ℕ → ( 0 C 𝐾 ) = 0 )