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 ⊢φ→C∈ℂ∖K−1
bccm1k.k ⊢φ→K∈ℕ
Assertion bccm1k ⊢φ→CC𝑐K−1=CC𝑐KC−K−1K

Proof

Step Hyp Ref Expression
1 bccm1k.c ⊢φ→C∈ℂ∖K−1
2 bccm1k.k ⊢φ→K∈ℕ
3 1 eldifad ⊢φ→C∈ℂ
4 2 nncnd ⊢φ→K∈ℂ
5 1cnd ⊢φ→1∈ℂ
6 4 5 subcld ⊢φ→K−1∈ℂ
7 3 6 subcld ⊢φ→C−K−1∈ℂ
8 2 nnne0d ⊢φ→K≠0
9 7 4 8 divcld ⊢φ→C−K−1K∈ℂ
10 nnm1nn0 ⊢K∈ℕ→K−1∈ℕ0
11 2 10 syl ⊢φ→K−1∈ℕ0
12 3 11 bcccl ⊢φ→CC𝑐K−1∈ℂ
13 eldifsni ⊢C∈ℂ∖K−1→C≠K−1
14 1 13 syl ⊢φ→C≠K−1
15 3 6 14 subne0d ⊢φ→C−K−1≠0
16 7 4 15 8 divne0d ⊢φ→C−K−1K≠0
17 3 11 bccp1k ⊢φ→CC𝑐K-1+1=CC𝑐K−1⁢C−K−1K-1+1
18 4 5 npcand ⊢φ→K-1+1=K
19 18 oveq2d ⊢φ→CC𝑐K-1+1=CC𝑐K
20 18 oveq2d ⊢φ→C−K−1K-1+1=C−K−1K
21 20 oveq2d ⊢φ→CC𝑐K−1⁢C−K−1K-1+1=CC𝑐K−1⁢C−K−1K
22 17 19 21 3eqtr3d ⊢φ→CC𝑐K=CC𝑐K−1⁢C−K−1K
23 12 9 mulcomd ⊢φ→CC𝑐K−1⁢C−K−1K=C−K−1K⁢CC𝑐K−1
24 22 23 eqtr2d ⊢φ→C−K−1K⁢CC𝑐K−1=CC𝑐K
25 9 12 16 24 mvllmuld ⊢φ→CC𝑐K−1=CC𝑐KC−K−1K