This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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