Metamath Proof Explorer


Theorem 6rp

Description: 6 is a positive real. (Contributed by SN, 26-Aug-2025)

Ref Expression
Assertion 6rp
|- 6 e. RR+

Proof

Step Hyp Ref Expression
1 6re
 |-  6 e. RR
2 6pos
 |-  0 < 6
3 1 2 elrpii
 |-  6 e. RR+