Metamath Proof Explorer

Theorem bccp1k

Description: Generalized binomial coefficient: C choose ( K + 1 ) . (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses bccval.c 
|- ( ph -> C e. CC )
bccval.k 
|- ( ph -> K e. NN0 )
Assertion bccp1k 
|- ( ph -> ( C _Cc ( K + 1 ) ) = ( ( C _Cc K ) x. ( ( C - K ) / ( K + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 bccval.c 
 |-  ( ph -> C e. CC )
2 bccval.k 
 |-  ( ph -> K e. NN0 )
3 fallfacp1 
 |-  ( ( C e. CC /\ K e. NN0 ) -> ( C FallFac ( K + 1 ) ) = ( ( C FallFac K ) x. ( C - K ) ) )
4 1 2 3 syl2anc 
 |-  ( ph -> ( C FallFac ( K + 1 ) ) = ( ( C FallFac K ) x. ( C - K ) ) )
5 facp1 
 |-  ( K e. NN0 -> ( ! ` ( K + 1 ) ) = ( ( ! ` K ) x. ( K + 1 ) ) )
6 2 5 syl 
 |-  ( ph -> ( ! ` ( K + 1 ) ) = ( ( ! ` K ) x. ( K + 1 ) ) )
7 4 6 oveq12d 
 |-  ( ph -> ( ( C FallFac ( K + 1 ) ) / ( ! ` ( K + 1 ) ) ) = ( ( ( C FallFac K ) x. ( C - K ) ) / ( ( ! ` K ) x. ( K + 1 ) ) ) )
8 peano2nn0 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN0 )
9 2 8 syl 
 |-  ( ph -> ( K + 1 ) e. NN0 )
10 1 9 bccval 
 |-  ( ph -> ( C _Cc ( K + 1 ) ) = ( ( C FallFac ( K + 1 ) ) / ( ! ` ( K + 1 ) ) ) )
11 fallfaccl 
 |-  ( ( C e. CC /\ K e. NN0 ) -> ( C FallFac K ) e. CC )
12 1 2 11 syl2anc 
 |-  ( ph -> ( C FallFac K ) e. CC )
13 faccl 
 |-  ( K e. NN0 -> ( ! ` K ) e. NN )
14 2 13 syl 
 |-  ( ph -> ( ! ` K ) e. NN )
15 14 nncnd 
 |-  ( ph -> ( ! ` K ) e. CC )
16 2 nn0cnd 
 |-  ( ph -> K e. CC )
17 1 16 subcld 
 |-  ( ph -> ( C - K ) e. CC )
18 9 nn0cnd 
 |-  ( ph -> ( K + 1 ) e. CC )
19 14 nnne0d 
 |-  ( ph -> ( ! ` K ) =/= 0 )
20 nn0p1nn 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN )
21 2 20 syl 
 |-  ( ph -> ( K + 1 ) e. NN )
22 21 nnne0d 
 |-  ( ph -> ( K + 1 ) =/= 0 )
23 12 15 17 18 19 22 divmuldivd 
 |-  ( ph -> ( ( ( C FallFac K ) / ( ! ` K ) ) x. ( ( C - K ) / ( K + 1 ) ) ) = ( ( ( C FallFac K ) x. ( C - K ) ) / ( ( ! ` K ) x. ( K + 1 ) ) ) )
24 7 10 23 3eqtr4d 
 |-  ( ph -> ( C _Cc ( K + 1 ) ) = ( ( ( C FallFac K ) / ( ! ` K ) ) x. ( ( C - K ) / ( K + 1 ) ) ) )
25 1 2 bccval 
 |-  ( ph -> ( C _Cc K ) = ( ( C FallFac K ) / ( ! ` K ) ) )
26 25 oveq1d 
 |-  ( ph -> ( ( C _Cc K ) x. ( ( C - K ) / ( K + 1 ) ) ) = ( ( ( C FallFac K ) / ( ! ` K ) ) x. ( ( C - K ) / ( K + 1 ) ) ) )
27 24 26 eqtr4d 
 |-  ( ph -> ( C _Cc ( K + 1 ) ) = ( ( C _Cc K ) x. ( ( C - K ) / ( K + 1 ) ) ) )