# Metamath Proof Explorer

## Theorem bcval3

Description: Value of the binomial coefficient, N choose K , outside of its standard domain. Remark in Gleason p. 295. (Contributed by NM, 14-Jul-2005) (Revised by Mario Carneiro, 8-Nov-2013)

Ref Expression
Assertion bcval3 ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\wedge ¬{K}\in \left(0\dots {N}\right)\right)\to \left(\genfrac{}{}{0}{}{{N}}{{K}}\right)=0$

### Proof

Step Hyp Ref Expression
1 bcval ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\to \left(\genfrac{}{}{0}{}{{N}}{{K}}\right)=if\left({K}\in \left(0\dots {N}\right),\frac{{N}!}{\left({N}-{K}\right)!{K}!},0\right)$
2 1 3adant3 ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\wedge ¬{K}\in \left(0\dots {N}\right)\right)\to \left(\genfrac{}{}{0}{}{{N}}{{K}}\right)=if\left({K}\in \left(0\dots {N}\right),\frac{{N}!}{\left({N}-{K}\right)!{K}!},0\right)$
3 iffalse ${⊢}¬{K}\in \left(0\dots {N}\right)\to if\left({K}\in \left(0\dots {N}\right),\frac{{N}!}{\left({N}-{K}\right)!{K}!},0\right)=0$
4 3 3ad2ant3 ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\wedge ¬{K}\in \left(0\dots {N}\right)\right)\to if\left({K}\in \left(0\dots {N}\right),\frac{{N}!}{\left({N}-{K}\right)!{K}!},0\right)=0$
5 2 4 eqtrd ${⊢}\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\wedge ¬{K}\in \left(0\dots {N}\right)\right)\to \left(\genfrac{}{}{0}{}{{N}}{{K}}\right)=0$