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