Metamath Proof Explorer

Theorem bcfallfac

Description: Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018)

Ref Expression
Assertion bcfallfac 
|- ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( N FallFac K ) / ( ! ` K ) ) )

Proof

Step Hyp Ref Expression
1 elfz3nn0 
 |-  ( K e. ( 0 ... N ) -> N e. NN0 )
2 1 faccld 
 |-  ( K e. ( 0 ... N ) -> ( ! ` N ) e. NN )
3 2 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( ! ` N ) e. CC )
4 fznn0sub 
 |-  ( K e. ( 0 ... N ) -> ( N - K ) e. NN0 )
5 4 faccld 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( N - K ) ) e. NN )
6 5 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( N - K ) ) e. CC )
7 elfznn0 
 |-  ( K e. ( 0 ... N ) -> K e. NN0 )
8 7 faccld 
 |-  ( K e. ( 0 ... N ) -> ( ! ` K ) e. NN )
9 8 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( ! ` K ) e. CC )
10 5 nnne0d 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( N - K ) ) =/= 0 )
11 8 nnne0d 
 |-  ( K e. ( 0 ... N ) -> ( ! ` K ) =/= 0 )
12 3 6 9 10 11 divdiv1d 
 |-  ( K e. ( 0 ... N ) -> ( ( ( ! ` N ) / ( ! ` ( N - K ) ) ) / ( ! ` K ) ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
13 fallfacval4 
 |-  ( K e. ( 0 ... N ) -> ( N FallFac K ) = ( ( ! ` N ) / ( ! ` ( N - K ) ) ) )
14 13 oveq1d 
 |-  ( K e. ( 0 ... N ) -> ( ( N FallFac K ) / ( ! ` K ) ) = ( ( ( ! ` N ) / ( ! ` ( N - K ) ) ) / ( ! ` K ) ) )
15 bcval2 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
16 12 14 15 3eqtr4rd 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( N FallFac K ) / ( ! ` K ) ) )