Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Ordering on reals (cont.)
1le1
Next ⟩
Reciprocals
Metamath Proof Explorer
Ascii
Unicode
Theorem
1le1
Description:
One is less than or equal to one.
(Contributed by
David A. Wheeler
, 16-Jul-2016)
Ref
Expression
Assertion
1le1
⊢
1
≤
1
Proof
Step
Hyp
Ref
Expression
1
1re
⊢
1
∈
ℝ
2
1
leidi
⊢
1
≤
1