Metamath Proof Explorer


Theorem bcctr

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

Ref Expression
Assertion bcctr N 0 ( 2 N N) = 2 N ! N ! N !

Proof

Step Hyp Ref Expression
1 fzctr N 0 N 0 2 N
2 bcval2 N 0 2 N ( 2 N N) = 2 N ! 2 N N ! N !
3 1 2 syl N 0 ( 2 N N) = 2 N ! 2 N N ! N !
4 nn0cn N 0 N
5 4 2timesd N 0 2 N = N + N
6 4 4 5 mvrladdd N 0 2 N N = N
7 6 fveq2d N 0 2 N N ! = N !
8 7 oveq1d N 0 2 N N ! N ! = N ! N !
9 8 oveq2d N 0 2 N ! 2 N N ! N ! = 2 N ! N ! N !
10 3 9 eqtrd N 0 ( 2 N N) = 2 N ! N ! N !