Metamath Proof Explorer

Theorem bccval

Description: Value of the generalized binomial coefficient, C choose K . (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses bccval.c 
|- ( ph -> C e. CC )
bccval.k 
|- ( ph -> K e. NN0 )
Assertion bccval 
|- ( ph -> ( C _Cc K ) = ( ( C FallFac K ) / ( ! ` K ) ) )

Proof

Step Hyp Ref Expression
1 bccval.c 
 |-  ( ph -> C e. CC )
2 bccval.k 
 |-  ( ph -> K e. NN0 )
3 df-bcc 
 |-  _Cc = ( c e. CC , k e. NN0 |-> ( ( c FallFac k ) / ( ! ` k ) ) )
4 3 a1i 
 |-  ( ph -> _Cc = ( c e. CC , k e. NN0 |-> ( ( c FallFac k ) / ( ! ` k ) ) ) )
5 simprl 
 |-  ( ( ph /\ ( c = C /\ k = K ) ) -> c = C )
6 simprr 
 |-  ( ( ph /\ ( c = C /\ k = K ) ) -> k = K )
7 5 6 oveq12d 
 |-  ( ( ph /\ ( c = C /\ k = K ) ) -> ( c FallFac k ) = ( C FallFac K ) )
8 6 fveq2d 
 |-  ( ( ph /\ ( c = C /\ k = K ) ) -> ( ! ` k ) = ( ! ` K ) )
9 7 8 oveq12d 
 |-  ( ( ph /\ ( c = C /\ k = K ) ) -> ( ( c FallFac k ) / ( ! ` k ) ) = ( ( C FallFac K ) / ( ! ` K ) ) )
10 ovexd 
 |-  ( ph -> ( ( C FallFac K ) / ( ! ` K ) ) e. _V )
11 4 9 1 2 10 ovmpod 
 |-  ( ph -> ( C _Cc K ) = ( ( C FallFac K ) / ( ! ` K ) ) )