Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
4lt8
Next ⟩
3lt8
Metamath Proof Explorer
Ascii
Unicode
Theorem
4lt8
Description:
4 is less than 8.
(Contributed by
Mario Carneiro
, 15-Sep-2013)
Ref
Expression
Assertion
4lt8
⊢
4
<
8
Proof
Step
Hyp
Ref
Expression
1
4lt5
⊢
4
<
5
2
5lt8
⊢
5
<
8
3
4re
⊢
4
∈
ℝ
4
5re
⊢
5
∈
ℝ
5
8re
⊢
8
∈
ℝ
6
3
4
5
lttri
⊢
4
<
5
∧
5
<
8
→
4
<
8
7
1
2
6
mp2an
⊢
4
<
8