Database
REAL AND COMPLEX NUMBERS
Order sets
Positive reals (as a subset of complex numbers)
3rp
Next ⟩
rpssre
Metamath Proof Explorer
Ascii
Unicode
Theorem
3rp
Description:
3 is a positive real.
(Contributed by
Glauco Siliprandi
, 11-Dec-2019)
Ref
Expression
Assertion
3rp
⊢
3
∈
ℝ
+
Proof
Step
Hyp
Ref
Expression
1
3re
⊢
3
∈
ℝ
2
3pos
⊢
0
<
3
3
1
2
elrpii
⊢
3
∈
ℝ
+