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	⊢ ( 𝜑 → 𝐶 ∈ ( ℂ ∖ { ( 𝐾 − 1 ) } ) )
	bccm1k.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
Assertion	bccm1k	⊢ ( 𝜑 → ( 𝐶 C𝑐 ( 𝐾 − 1 ) ) = ( ( 𝐶 C𝑐 𝐾 ) / ( ( 𝐶 − ( 𝐾 − 1 ) ) / 𝐾 ) ) )

Proof

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