Theorem bcctr

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

	Ref	Expression
Assertion	bcctr	$$⊢N\in {\mathbb{N}}_0\to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}!}{N!N!}$$

Proof

Step	Hyp	Ref	Expression
1		fzctr	$$⊢N\in {\mathbb{N}}_0\to N\in \left(0\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
2		bcval2	$$⊢N\in \left(0\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}!}{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N\right)!N!}$$
3	1 2	syl	$$⊢N\in {\mathbb{N}}_0\to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}!}{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N\right)!N!}$$
4		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
5	4	2timesd	$$⊢N\in {\mathbb{N}}_0\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N+N$$
6	4 4 5	mvrladdd	$$⊢N\in {\mathbb{N}}_0\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N=N$$
7	6	fveq2d	$$⊢N\in {\mathbb{N}}_0\to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N\right)!=N!$$
8	7	oveq1d	$$⊢N\in {\mathbb{N}}_0\to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N\right)!N!=N!N!$$
9	8	oveq2d	$$⊢N\in {\mathbb{N}}_0\to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}!}{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N\right)!N!}=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}!}{N!N!}$$
10	3 9	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}!}{N!N!}$$