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