Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
rpsscn
Next ⟩
4rp
Metamath Proof Explorer
Ascii
Structured
Theorem
rpsscn
Description:
The positive reals are a subset of the complex numbers.
(Contributed by
SN
, 1-Oct-2025)
Ref
Expression
Assertion
rpsscn
⊢
ℝ
+
⊆ ℂ
Proof
Step
Hyp
Ref
Expression
1
rpssre
⊢
ℝ
+
⊆ ℝ
2
ax-resscn
⊢
ℝ ⊆ ℂ
3
1
2
sstri
⊢
ℝ
+
⊆ ℂ