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