Metamath Proof Explorer

Theorem bcm1nt

Description: The proportion of one binomial coefficient to another with N decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020)

Ref Expression
Assertion bcm1nt 
|- ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( N _C K ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) )

Proof

Step Hyp Ref Expression
1 bcp1n 
 |-  ( K e. ( 0 ... ( N - 1 ) ) -> ( ( ( N - 1 ) + 1 ) _C K ) = ( ( ( N - 1 ) _C K ) x. ( ( ( N - 1 ) + 1 ) / ( ( ( N - 1 ) + 1 ) - K ) ) ) )
2 1 adantl 
 |-  ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( N - 1 ) + 1 ) _C K ) = ( ( ( N - 1 ) _C K ) x. ( ( ( N - 1 ) + 1 ) / ( ( ( N - 1 ) + 1 ) - K ) ) ) )
3 simpl 
 |-  ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> N e. NN )
4 3 nncnd 
 |-  ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> N e. CC )
5 1cnd 
 |-  ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> 1 e. CC )
6 4 5 npcand 
 |-  ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )
7 6 oveq1d 
 |-  ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( N - 1 ) + 1 ) _C K ) = ( N _C K ) )
8 6 oveq1d 
 |-  ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( N - 1 ) + 1 ) - K ) = ( N - K ) )
9 6 8 oveq12d 
 |-  ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( N - 1 ) + 1 ) / ( ( ( N - 1 ) + 1 ) - K ) ) = ( N / ( N - K ) ) )
10 9 oveq2d 
 |-  ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( N - 1 ) _C K ) x. ( ( ( N - 1 ) + 1 ) / ( ( ( N - 1 ) + 1 ) - K ) ) ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) )
11 2 7 10 3eqtr3d 
 |-  ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( N _C K ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) )