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 
|- ( ph -> C e. ( CC \ { ( K - 1 ) } ) )
bccm1k.k 
|- ( ph -> K e. NN )
Assertion bccm1k 
|- ( ph -> ( C _Cc ( K - 1 ) ) = ( ( C _Cc K ) / ( ( C - ( K - 1 ) ) / K ) ) )

Proof

Step Hyp Ref Expression
1 bccm1k.c 
 |-  ( ph -> C e. ( CC \ { ( K - 1 ) } ) )
2 bccm1k.k 
 |-  ( ph -> K e. NN )
3 1 eldifad 
 |-  ( ph -> C e. CC )
4 2 nncnd 
 |-  ( ph -> K e. CC )
5 1cnd 
 |-  ( ph -> 1 e. CC )
6 4 5 subcld 
 |-  ( ph -> ( K - 1 ) e. CC )
7 3 6 subcld 
 |-  ( ph -> ( C - ( K - 1 ) ) e. CC )
8 2 nnne0d 
 |-  ( ph -> K =/= 0 )
9 7 4 8 divcld 
 |-  ( ph -> ( ( C - ( K - 1 ) ) / K ) e. CC )
10 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
11 2 10 syl 
 |-  ( ph -> ( K - 1 ) e. NN0 )
12 3 11 bcccl 
 |-  ( ph -> ( C _Cc ( K - 1 ) ) e. CC )
13 eldifsni 
 |-  ( C e. ( CC \ { ( K - 1 ) } ) -> C =/= ( K - 1 ) )
14 1 13 syl 
 |-  ( ph -> C =/= ( K - 1 ) )
15 3 6 14 subne0d 
 |-  ( ph -> ( C - ( K - 1 ) ) =/= 0 )
16 7 4 15 8 divne0d 
 |-  ( ph -> ( ( C - ( K - 1 ) ) / K ) =/= 0 )
17 3 11 bccp1k 
 |-  ( ph -> ( C _Cc ( ( K - 1 ) + 1 ) ) = ( ( C _Cc ( K - 1 ) ) x. ( ( C - ( K - 1 ) ) / ( ( K - 1 ) + 1 ) ) ) )
18 4 5 npcand 
 |-  ( ph -> ( ( K - 1 ) + 1 ) = K )
19 18 oveq2d 
 |-  ( ph -> ( C _Cc ( ( K - 1 ) + 1 ) ) = ( C _Cc K ) )
20 18 oveq2d 
 |-  ( ph -> ( ( C - ( K - 1 ) ) / ( ( K - 1 ) + 1 ) ) = ( ( C - ( K - 1 ) ) / K ) )
21 20 oveq2d 
 |-  ( ph -> ( ( C _Cc ( K - 1 ) ) x. ( ( C - ( K - 1 ) ) / ( ( K - 1 ) + 1 ) ) ) = ( ( C _Cc ( K - 1 ) ) x. ( ( C - ( K - 1 ) ) / K ) ) )
22 17 19 21 3eqtr3d 
 |-  ( ph -> ( C _Cc K ) = ( ( C _Cc ( K - 1 ) ) x. ( ( C - ( K - 1 ) ) / K ) ) )
23 12 9 mulcomd 
 |-  ( ph -> ( ( C _Cc ( K - 1 ) ) x. ( ( C - ( K - 1 ) ) / K ) ) = ( ( ( C - ( K - 1 ) ) / K ) x. ( C _Cc ( K - 1 ) ) ) )
24 22 23 eqtr2d 
 |-  ( ph -> ( ( ( C - ( K - 1 ) ) / K ) x. ( C _Cc ( K - 1 ) ) ) = ( C _Cc K ) )
25 9 12 16 24 mvllmuld 
 |-  ( ph -> ( C _Cc ( K - 1 ) ) = ( ( C _Cc K ) / ( ( C - ( K - 1 ) ) / K ) ) )