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