Database
REAL AND COMPLEX NUMBERS
Order sets
Positive reals (as a subset of complex numbers)
rpssre
Next ⟩
rpre
Metamath Proof Explorer
Ascii
Unicode
Theorem
rpssre
Description:
The positive reals are a subset of the reals.
(Contributed by
NM
, 24-Feb-2008)
Ref
Expression
Assertion
rpssre
⊢
ℝ
+
⊆
ℝ
Proof
Step
Hyp
Ref
Expression
1
df-rp
⊢
ℝ
+
=
x
∈
ℝ
|
0
<
x
2
1
ssrab3
⊢
ℝ
+
⊆
ℝ