Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
1le3
Next ⟩
neg1mulneg1e1
Metamath Proof Explorer
Ascii
Unicode
Theorem
1le3
Description:
1 is less than or equal to 3.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
1le3
⊢
1
≤
3
Proof
Step
Hyp
Ref
Expression
1
1re
⊢
1
∈
ℝ
2
3re
⊢
3
∈
ℝ
3
1lt3
⊢
1
<
3
4
1
2
3
ltleii
⊢
1
≤
3