Theorem bcctr

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

	Ref	Expression
Assertion	bcctr	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fzctr	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) )
2		bcval2	⊢ ( 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ ( ( 2 · 𝑁 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ ( ( 2 · 𝑁 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
4		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
5	4	2timesd	⊢ ( 𝑁 ∈ ℕ0 → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
6	4 4 5	mvrladdd	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) − 𝑁 ) = 𝑁 )
7	6	fveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( ( 2 · 𝑁 ) − 𝑁 ) ) = ( ! ‘ 𝑁 ) )
8	7	oveq1d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ ( ( 2 · 𝑁 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) = ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) )
9	8	oveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ ( ( 2 · 𝑁 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
10	3 9	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )