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 ( 0 K) = 0

Proof

Step Hyp Ref Expression
1 0nn0 0 0
2 nnz K K
3 nngt0 K 0 < K
4 3 olcd K K < 0 0 < K
5 bcval4 0 0 K K < 0 0 < K ( 0 K) = 0
6 1 2 4 5 mp3an2i K ( 0 K) = 0