Metamath Proof Explorer

Theorem bccm1k

Description: Generalized binomial coefficient: C choose ( K - 1 ) , when C is not ( K - 1 ) . (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses bccm1k.c ${⊢}{\phi }\to {C}\in \left(ℂ\setminus \left\{{K}-1\right\}\right)$
bccm1k.k ${⊢}{\phi }\to {K}\in ℕ$
Assertion bccm1k ${⊢}{\phi }\to {C}{C}_{𝑐}\left({K}-1\right)=\frac{{C}{C}_{𝑐}{K}}{\frac{{C}-\left({K}-1\right)}{{K}}}$

Proof

Step Hyp Ref Expression
1 bccm1k.c ${⊢}{\phi }\to {C}\in \left(ℂ\setminus \left\{{K}-1\right\}\right)$
2 bccm1k.k ${⊢}{\phi }\to {K}\in ℕ$
3 1 eldifad ${⊢}{\phi }\to {C}\in ℂ$
4 2 nncnd ${⊢}{\phi }\to {K}\in ℂ$
5 1cnd ${⊢}{\phi }\to 1\in ℂ$
6 4 5 subcld ${⊢}{\phi }\to {K}-1\in ℂ$
7 3 6 subcld ${⊢}{\phi }\to {C}-\left({K}-1\right)\in ℂ$
8 2 nnne0d ${⊢}{\phi }\to {K}\ne 0$
9 7 4 8 divcld ${⊢}{\phi }\to \frac{{C}-\left({K}-1\right)}{{K}}\in ℂ$
10 nnm1nn0 ${⊢}{K}\in ℕ\to {K}-1\in {ℕ}_{0}$
11 2 10 syl ${⊢}{\phi }\to {K}-1\in {ℕ}_{0}$
12 3 11 bcccl ${⊢}{\phi }\to {C}{C}_{𝑐}\left({K}-1\right)\in ℂ$
13 eldifsni ${⊢}{C}\in \left(ℂ\setminus \left\{{K}-1\right\}\right)\to {C}\ne {K}-1$
14 1 13 syl ${⊢}{\phi }\to {C}\ne {K}-1$
15 3 6 14 subne0d ${⊢}{\phi }\to {C}-\left({K}-1\right)\ne 0$
16 7 4 15 8 divne0d ${⊢}{\phi }\to \frac{{C}-\left({K}-1\right)}{{K}}\ne 0$
17 3 11 bccp1k ${⊢}{\phi }\to {C}{C}_{𝑐}\left({K}-1+1\right)=\left({C}{C}_{𝑐}\left({K}-1\right)\right)\left(\frac{{C}-\left({K}-1\right)}{{K}-1+1}\right)$
18 4 5 npcand ${⊢}{\phi }\to {K}-1+1={K}$
19 18 oveq2d ${⊢}{\phi }\to {C}{C}_{𝑐}\left({K}-1+1\right)={C}{C}_{𝑐}{K}$
20 18 oveq2d ${⊢}{\phi }\to \frac{{C}-\left({K}-1\right)}{{K}-1+1}=\frac{{C}-\left({K}-1\right)}{{K}}$
21 20 oveq2d ${⊢}{\phi }\to \left({C}{C}_{𝑐}\left({K}-1\right)\right)\left(\frac{{C}-\left({K}-1\right)}{{K}-1+1}\right)=\left({C}{C}_{𝑐}\left({K}-1\right)\right)\left(\frac{{C}-\left({K}-1\right)}{{K}}\right)$
22 17 19 21 3eqtr3d ${⊢}{\phi }\to {C}{C}_{𝑐}{K}=\left({C}{C}_{𝑐}\left({K}-1\right)\right)\left(\frac{{C}-\left({K}-1\right)}{{K}}\right)$
23 12 9 mulcomd ${⊢}{\phi }\to \left({C}{C}_{𝑐}\left({K}-1\right)\right)\left(\frac{{C}-\left({K}-1\right)}{{K}}\right)=\left(\frac{{C}-\left({K}-1\right)}{{K}}\right)\left({C}{C}_{𝑐}\left({K}-1\right)\right)$
24 22 23 eqtr2d ${⊢}{\phi }\to \left(\frac{{C}-\left({K}-1\right)}{{K}}\right)\left({C}{C}_{𝑐}\left({K}-1\right)\right)={C}{C}_{𝑐}{K}$
25 9 12 16 24 mvllmuld ${⊢}{\phi }\to {C}{C}_{𝑐}\left({K}-1\right)=\frac{{C}{C}_{𝑐}{K}}{\frac{{C}-\left({K}-1\right)}{{K}}}$