Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic number theory
Bertrand's postulate
bcctr
Next ⟩
pcbcctr
Metamath Proof Explorer
Ascii
Unicode
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
!