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