# Metamath Proof Explorer

## Theorem bccbc

Description: The binomial coefficient and generalized binomial coefficient are equal when their arguments are nonnegative integers. (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses bccbc.c ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
bccbc.k ${⊢}{\phi }\to {K}\in {ℕ}_{0}$
Assertion bccbc ${⊢}{\phi }\to {N}{C}_{𝑐}{K}=\left(\genfrac{}{}{0}{}{{N}}{{K}}\right)$

### Proof

Step Hyp Ref Expression
1 bccbc.c ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
2 bccbc.k ${⊢}{\phi }\to {K}\in {ℕ}_{0}$
3 1 nn0cnd ${⊢}{\phi }\to {N}\in ℂ$
4 3 2 bccval ${⊢}{\phi }\to {N}{C}_{𝑐}{K}=\frac{{{N}}^{\underset{_}{{K}}}}{{K}!}$
5 4 adantr ${⊢}\left({\phi }\wedge {K}\in \left(0\dots {N}\right)\right)\to {N}{C}_{𝑐}{K}=\frac{{{N}}^{\underset{_}{{K}}}}{{K}!}$
6 bcfallfac ${⊢}{K}\in \left(0\dots {N}\right)\to \left(\genfrac{}{}{0}{}{{N}}{{K}}\right)=\frac{{{N}}^{\underset{_}{{K}}}}{{K}!}$
7 6 adantl ${⊢}\left({\phi }\wedge {K}\in \left(0\dots {N}\right)\right)\to \left(\genfrac{}{}{0}{}{{N}}{{K}}\right)=\frac{{{N}}^{\underset{_}{{K}}}}{{K}!}$
8 5 7 eqtr4d ${⊢}\left({\phi }\wedge {K}\in \left(0\dots {N}\right)\right)\to {N}{C}_{𝑐}{K}=\left(\genfrac{}{}{0}{}{{N}}{{K}}\right)$
9 nn0split ${⊢}{N}\in {ℕ}_{0}\to {ℕ}_{0}=\left(0\dots {N}\right)\cup {ℤ}_{\ge \left({N}+1\right)}$
10 1 9 syl ${⊢}{\phi }\to {ℕ}_{0}=\left(0\dots {N}\right)\cup {ℤ}_{\ge \left({N}+1\right)}$
11 2 10 eleqtrd ${⊢}{\phi }\to {K}\in \left(\left(0\dots {N}\right)\cup {ℤ}_{\ge \left({N}+1\right)}\right)$
12 elun ${⊢}{K}\in \left(\left(0\dots {N}\right)\cup {ℤ}_{\ge \left({N}+1\right)}\right)↔\left({K}\in \left(0\dots {N}\right)\vee {K}\in {ℤ}_{\ge \left({N}+1\right)}\right)$
13 11 12 sylib ${⊢}{\phi }\to \left({K}\in \left(0\dots {N}\right)\vee {K}\in {ℤ}_{\ge \left({N}+1\right)}\right)$
14 13 orcanai ${⊢}\left({\phi }\wedge ¬{K}\in \left(0\dots {N}\right)\right)\to {K}\in {ℤ}_{\ge \left({N}+1\right)}$
15 eluzle ${⊢}{K}\in {ℤ}_{\ge \left({N}+1\right)}\to {N}+1\le {K}$
16 15 adantl ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {N}+1\le {K}$
17 1 nn0zd ${⊢}{\phi }\to {N}\in ℤ$
18 2 nn0zd ${⊢}{\phi }\to {K}\in ℤ$
19 zltp1le ${⊢}\left({N}\in ℤ\wedge {K}\in ℤ\right)\to \left({N}<{K}↔{N}+1\le {K}\right)$
20 17 18 19 syl2anc ${⊢}{\phi }\to \left({N}<{K}↔{N}+1\le {K}\right)$
21 20 adantr ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({N}<{K}↔{N}+1\le {K}\right)$
22 16 21 mpbird ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {N}<{K}$
23 14 22 syldan ${⊢}\left({\phi }\wedge ¬{K}\in \left(0\dots {N}\right)\right)\to {N}<{K}$
24 1 nn0ge0d ${⊢}{\phi }\to 0\le {N}$
25 0zd ${⊢}{\phi }\to 0\in ℤ$
26 elfzo ${⊢}\left({N}\in ℤ\wedge 0\in ℤ\wedge {K}\in ℤ\right)\to \left({N}\in \left(0..^{K}\right)↔\left(0\le {N}\wedge {N}<{K}\right)\right)$
27 17 25 18 26 syl3anc ${⊢}{\phi }\to \left({N}\in \left(0..^{K}\right)↔\left(0\le {N}\wedge {N}<{K}\right)\right)$
28 27 biimpar ${⊢}\left({\phi }\wedge \left(0\le {N}\wedge {N}<{K}\right)\right)\to {N}\in \left(0..^{K}\right)$
29 fzoval ${⊢}{K}\in ℤ\to \left(0..^{K}\right)=\left(0\dots {K}-1\right)$
30 18 29 syl ${⊢}{\phi }\to \left(0..^{K}\right)=\left(0\dots {K}-1\right)$
31 30 eleq2d ${⊢}{\phi }\to \left({N}\in \left(0..^{K}\right)↔{N}\in \left(0\dots {K}-1\right)\right)$
32 31 biimpa ${⊢}\left({\phi }\wedge {N}\in \left(0..^{K}\right)\right)\to {N}\in \left(0\dots {K}-1\right)$
33 3 2 bcc0 ${⊢}{\phi }\to \left({N}{C}_{𝑐}{K}=0↔{N}\in \left(0\dots {K}-1\right)\right)$
34 33 biimpar ${⊢}\left({\phi }\wedge {N}\in \left(0\dots {K}-1\right)\right)\to {N}{C}_{𝑐}{K}=0$
35 32 34 syldan ${⊢}\left({\phi }\wedge {N}\in \left(0..^{K}\right)\right)\to {N}{C}_{𝑐}{K}=0$
36 28 35 syldan ${⊢}\left({\phi }\wedge \left(0\le {N}\wedge {N}<{K}\right)\right)\to {N}{C}_{𝑐}{K}=0$
37 24 36 sylanr1 ${⊢}\left({\phi }\wedge \left({\phi }\wedge {N}<{K}\right)\right)\to {N}{C}_{𝑐}{K}=0$
38 37 anabss5 ${⊢}\left({\phi }\wedge {N}<{K}\right)\to {N}{C}_{𝑐}{K}=0$
39 23 38 syldan ${⊢}\left({\phi }\wedge ¬{K}\in \left(0\dots {N}\right)\right)\to {N}{C}_{𝑐}{K}=0$
40 1 18 jca ${⊢}{\phi }\to \left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)$
41 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$
42 41 3expa ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {K}\in ℤ\right)\wedge ¬{K}\in \left(0\dots {N}\right)\right)\to \left(\genfrac{}{}{0}{}{{N}}{{K}}\right)=0$
43 40 42 sylan ${⊢}\left({\phi }\wedge ¬{K}\in \left(0\dots {N}\right)\right)\to \left(\genfrac{}{}{0}{}{{N}}{{K}}\right)=0$
44 39 43 eqtr4d ${⊢}\left({\phi }\wedge ¬{K}\in \left(0\dots {N}\right)\right)\to {N}{C}_{𝑐}{K}=\left(\genfrac{}{}{0}{}{{N}}{{K}}\right)$
45 8 44 pm2.61dan ${⊢}{\phi }\to {N}{C}_{𝑐}{K}=\left(\genfrac{}{}{0}{}{{N}}{{K}}\right)$