Metamath Proof Explorer


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 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )