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 ( 𝐾 ∈ ℕ → ( 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 )