Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
The binomial coefficient operation
4bc3eq4
Next ⟩
4bc2eq6
Metamath Proof Explorer
Ascii
Unicode
Theorem
4bc3eq4
Description:
The value of four choose three.
(Contributed by
Scott Fenton
, 11-Jun-2016)
Ref
Expression
Assertion
4bc3eq4
⊢
(
4
3
)
=
4
Proof
Step
Hyp
Ref
Expression
1
4m1e3
⊢
4
−
1
=
3
2
1
oveq2i
⊢
(
4
4
−
1
)
=
(
4
3
)
3
4nn0
⊢
4
∈
ℕ
0
4
bcnm1
⊢
4
∈
ℕ
0
→
(
4
4
−
1
)
=
4
5
3
4
ax-mp
⊢
(
4
4
−
1
)
=
4
6
2
5
eqtr3i
⊢
(
4
3
)
=
4