Metamath Proof Explorer

Theorem bcctr

Description: Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion bcctr 
|- ( N e. NN0 -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )

Proof

Step Hyp Ref Expression
1 fzctr 
 |-  ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
2 bcval2 
 |-  ( N e. ( 0 ... ( 2 x. N ) ) -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` ( ( 2 x. N ) - N ) ) x. ( ! ` N ) ) ) )
3 1 2 syl 
 |-  ( N e. NN0 -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` ( ( 2 x. N ) - N ) ) x. ( ! ` N ) ) ) )
4 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
5 4 2timesd 
 |-  ( N e. NN0 -> ( 2 x. N ) = ( N + N ) )
6 4 4 5 mvrladdd 
 |-  ( N e. NN0 -> ( ( 2 x. N ) - N ) = N )
7 6 fveq2d 
 |-  ( N e. NN0 -> ( ! ` ( ( 2 x. N ) - N ) ) = ( ! ` N ) )
8 7 oveq1d 
 |-  ( N e. NN0 -> ( ( ! ` ( ( 2 x. N ) - N ) ) x. ( ! ` N ) ) = ( ( ! ` N ) x. ( ! ` N ) ) )
9 8 oveq2d 
 |-  ( N e. NN0 -> ( ( ! ` ( 2 x. N ) ) / ( ( ! ` ( ( 2 x. N ) - N ) ) x. ( ! ` N ) ) ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )
10 3 9 eqtrd 
 |-  ( N e. NN0 -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )