This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Elementary integer functions The binomial coefficient operation 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 )