Metamath Proof Explorer


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 ∈ ℝ +