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