Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
7rp
Next ⟩
8rp
Metamath Proof Explorer
Ascii
Unicode
Theorem
7rp
Description:
7 is a positive real.
(Contributed by
SN
, 26-Aug-2025)
Ref
Expression
Assertion
7rp
⊢
7
∈
ℝ
+
Proof
Step
Hyp
Ref
Expression
1
7re
⊢
7
∈
ℝ
2
7pos
⊢
0
<
7
3
1
2
elrpii
⊢
7
∈
ℝ
+