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 ) ) ) )