# Metamath Proof Explorer

## Theorem bccval

Description: Value of the generalized binomial coefficient, C choose K . (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses bccval.c ${⊢}{\phi }\to {C}\in ℂ$
bccval.k ${⊢}{\phi }\to {K}\in {ℕ}_{0}$
Assertion bccval ${⊢}{\phi }\to {C}{C}_{𝑐}{K}=\frac{{{C}}^{\underset{_}{{K}}}}{{K}!}$

### Proof

Step Hyp Ref Expression
1 bccval.c ${⊢}{\phi }\to {C}\in ℂ$
2 bccval.k ${⊢}{\phi }\to {K}\in {ℕ}_{0}$
3 df-bcc ${⊢}{C}_{𝑐}=\left({c}\in ℂ,{k}\in {ℕ}_{0}⟼\frac{{{c}}^{\underset{_}{{k}}}}{{k}!}\right)$
4 3 a1i ${⊢}{\phi }\to {C}_{𝑐}=\left({c}\in ℂ,{k}\in {ℕ}_{0}⟼\frac{{{c}}^{\underset{_}{{k}}}}{{k}!}\right)$
5 simprl ${⊢}\left({\phi }\wedge \left({c}={C}\wedge {k}={K}\right)\right)\to {c}={C}$
6 simprr ${⊢}\left({\phi }\wedge \left({c}={C}\wedge {k}={K}\right)\right)\to {k}={K}$
7 5 6 oveq12d ${⊢}\left({\phi }\wedge \left({c}={C}\wedge {k}={K}\right)\right)\to {{c}}^{\underset{_}{{k}}}={{C}}^{\underset{_}{{K}}}$
8 6 fveq2d ${⊢}\left({\phi }\wedge \left({c}={C}\wedge {k}={K}\right)\right)\to {k}!={K}!$
9 7 8 oveq12d ${⊢}\left({\phi }\wedge \left({c}={C}\wedge {k}={K}\right)\right)\to \frac{{{c}}^{\underset{_}{{k}}}}{{k}!}=\frac{{{C}}^{\underset{_}{{K}}}}{{K}!}$
10 ovexd ${⊢}{\phi }\to \frac{{{C}}^{\underset{_}{{K}}}}{{K}!}\in \mathrm{V}$
11 4 9 1 2 10 ovmpod ${⊢}{\phi }\to {C}{C}_{𝑐}{K}=\frac{{{C}}^{\underset{_}{{K}}}}{{K}!}$