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

Metamath Proof Explorer

Theorem bcval

Description: Value of the binomial coefficient, N choose K . Definition of binomial coefficient in Gleason p. 295. As suggested by Gleason, we define it to be 0 when 0 <_ K <_ N does not hold. See bcval2 for the value in the standard domain. (Contributed by NM, 10-Jul-2005) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion bcval 
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) = if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
2 1 eleq2d 
 |-  ( n = N -> ( k e. ( 0 ... n ) <-> k e. ( 0 ... N ) ) )
3 fveq2 
 |-  ( n = N -> ( ! ` n ) = ( ! ` N ) )
4 fvoveq1 
 |-  ( n = N -> ( ! ` ( n - k ) ) = ( ! ` ( N - k ) ) )
5 4 oveq1d 
 |-  ( n = N -> ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) = ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) )
6 3 5 oveq12d 
 |-  ( n = N -> ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) = ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) )
7 2 6 ifbieq1d 
 |-  ( n = N -> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) = if ( k e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) , 0 ) )
8 eleq1 
 |-  ( k = K -> ( k e. ( 0 ... N ) <-> K e. ( 0 ... N ) ) )
9 oveq2 
 |-  ( k = K -> ( N - k ) = ( N - K ) )
10 9 fveq2d 
 |-  ( k = K -> ( ! ` ( N - k ) ) = ( ! ` ( N - K ) ) )
11 fveq2 
 |-  ( k = K -> ( ! ` k ) = ( ! ` K ) )
12 10 11 oveq12d 
 |-  ( k = K -> ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) = ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) )
13 12 oveq2d 
 |-  ( k = K -> ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
14 8 13 ifbieq1d 
 |-  ( k = K -> if ( k e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) , 0 ) = if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) )
15 df-bc 
 |-  _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
16 ovex 
 |-  ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) e. _V
17 c0ex 
 |-  0 e. _V
18 16 17 ifex 
 |-  if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) e. _V
19 7 14 15 18 ovmpo 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) = if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) )