This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bcval2

Description: Value of the binomial coefficient, N choose K , in its standard domain. (Contributed by NM, 9-Jun-2005) (Revised by Mario Carneiro, 7-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 elfz3nn0 
 |-  ( K e. ( 0 ... N ) -> N e. NN0 )
2 elfzelz 
 |-  ( K e. ( 0 ... N ) -> K e. ZZ )
3 bcval 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) = if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) )
4 1 2 3 syl2anc 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) )
5 iftrue 
 |-  ( K e. ( 0 ... N ) -> if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
6 4 5 eqtrd 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )