Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for metakunt
Miscellaneous results for AKS formalisation
5bc2eq10
Next ⟩
facp2
Metamath Proof Explorer
Ascii
Unicode
Theorem
5bc2eq10
Description:
The value of 5 choose 2.
(Contributed by
metakunt
, 8-Jun-2024)
Ref
Expression
Assertion
5bc2eq10
⊢
(
5
2
)
=
10
Proof
Step
Hyp
Ref
Expression
1
4nn0
⊢
4
∈
ℕ
0
2
2z
⊢
2
∈
ℤ
3
bcpasc
⊢
4
∈
ℕ
0
∧
2
∈
ℤ
→
(
4
2
)
+
(
4
2
−
1
)
=
(
4
+
1
2
)
4
1
2
3
mp2an
⊢
(
4
2
)
+
(
4
2
−
1
)
=
(
4
+
1
2
)
5
4p1e5
⊢
4
+
1
=
5
6
5
oveq1i
⊢
(
4
+
1
2
)
=
(
5
2
)
7
4
6
eqtri
⊢
(
4
2
)
+
(
4
2
−
1
)
=
(
5
2
)
8
7
eqcomi
⊢
(
5
2
)
=
(
4
2
)
+
(
4
2
−
1
)
9
2m1e1
⊢
2
−
1
=
1
10
9
oveq2i
⊢
(
4
2
−
1
)
=
(
4
1
)
11
10
oveq2i
⊢
(
4
2
)
+
(
4
2
−
1
)
=
(
4
2
)
+
(
4
1
)
12
4bc2eq6
⊢
(
4
2
)
=
6
13
bcn1
⊢
4
∈
ℕ
0
→
(
4
1
)
=
4
14
1
13
ax-mp
⊢
(
4
1
)
=
4
15
12
14
oveq12i
⊢
(
4
2
)
+
(
4
1
)
=
6
+
4
16
11
15
eqtri
⊢
(
4
2
)
+
(
4
2
−
1
)
=
6
+
4
17
6p4e10
⊢
6
+
4
=
10
18
8
16
17
3eqtri
⊢
(
5
2
)
=
10