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 ⊢ φ → C C 𝑐 K − 1 = C C 𝑐 K C − K − 1 K

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 − 1 K ∈ ℂ
10 nnm1nn0 ⊢ K ∈ ℕ → K − 1 ∈ ℕ 0
11 2 10 syl ⊢ φ → K − 1 ∈ ℕ 0
12 3 11 bcccl ⊢ φ → C C 𝑐 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 − 1 K ≠ 0
17 3 11 bccp1k ⊢ φ → C C 𝑐 K - 1 + 1 = C C 𝑐 K − 1 ⁢ C − K − 1 K - 1 + 1
18 4 5 npcand ⊢ φ → K - 1 + 1 = K
19 18 oveq2d ⊢ φ → C C 𝑐 K - 1 + 1 = C C 𝑐 K
20 18 oveq2d ⊢ φ → C − K − 1 K - 1 + 1 = C − K − 1 K
21 20 oveq2d ⊢ φ → C C 𝑐 K − 1 ⁢ C − K − 1 K - 1 + 1 = C C 𝑐 K − 1 ⁢ C − K − 1 K
22 17 19 21 3eqtr3d ⊢ φ → C C 𝑐 K = C C 𝑐 K − 1 ⁢ C − K − 1 K
23 12 9 mulcomd ⊢ φ → C C 𝑐 K − 1 ⁢ C − K − 1 K = C − K − 1 K ⁢ C C 𝑐 K − 1
24 22 23 eqtr2d ⊢ φ → C − K − 1 K ⁢ C C 𝑐 K − 1 = C C 𝑐 K
25 9 12 16 24 mvllmuld ⊢ φ → C C 𝑐 K − 1 = C C 𝑐 K C − K − 1 K