Database
REAL AND COMPLEX NUMBERS
Order sets
Positive reals (as a subset of complex numbers)
1rp
Next ⟩
2rp
Metamath Proof Explorer
Ascii
Structured
Theorem
1rp
Description:
1 is a positive real.
(Contributed by
Jeff Hankins
, 23-Nov-2008)
Ref
Expression
Assertion
1rp
⊢
1 ∈ ℝ
^{+}
Proof
Step
Hyp
Ref
Expression
1
1re
⊢
1 ∈ ℝ
2
0lt1
⊢
0 < 1
3
1
2
elrpii
⊢
1 ∈ ℝ
^{+}