Metamath Proof Explorer


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