Metamath Proof Explorer

Theorem bcccl

Description: Closure of the generalized binomial coefficient. (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses bccval.c 
|- ( ph -> C e. CC )
bccval.k 
|- ( ph -> K e. NN0 )
Assertion bcccl 
|- ( ph -> ( C _Cc K ) e. CC )

Proof

Step Hyp Ref Expression
1 bccval.c 
 |-  ( ph -> C e. CC )
2 bccval.k 
 |-  ( ph -> K e. NN0 )
3 1 2 bccval 
 |-  ( ph -> ( C _Cc K ) = ( ( C FallFac K ) / ( ! ` K ) ) )
4 fallfaccl 
 |-  ( ( C e. CC /\ K e. NN0 ) -> ( C FallFac K ) e. CC )
5 1 2 4 syl2anc 
 |-  ( ph -> ( C FallFac K ) e. CC )
6 faccl 
 |-  ( K e. NN0 -> ( ! ` K ) e. NN )
7 2 6 syl 
 |-  ( ph -> ( ! ` K ) e. NN )
8 7 nncnd 
 |-  ( ph -> ( ! ` K ) e. CC )
9 7 nnne0d 
 |-  ( ph -> ( ! ` K ) =/= 0 )
10 5 8 9 divcld 
 |-  ( ph -> ( ( C FallFac K ) / ( ! ` K ) ) e. CC )
11 3 10 eqeltrd 
 |-  ( ph -> ( C _Cc K ) e. CC )