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 e. NN -> ( 0 _C K ) = 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0nn0 | |- 0 e. NN0 |
|
| 2 | nnz | |- ( K e. NN -> K e. ZZ ) |
|
| 3 | nngt0 | |- ( K e. NN -> 0 < K ) |
|
| 4 | 3 | olcd | |- ( K e. NN -> ( K < 0 \/ 0 < K ) ) |
| 5 | bcval4 | |- ( ( 0 e. NN0 /\ K e. ZZ /\ ( K < 0 \/ 0 < K ) ) -> ( 0 _C K ) = 0 ) |
|
| 6 | 1 2 4 5 | mp3an2i | |- ( K e. NN -> ( 0 _C K ) = 0 ) |