Metamath Proof Explorer


Theorem 1rp

Description: 1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008)

Ref Expression
Assertion 1rp 1 +

Proof

Step Hyp Ref Expression
1 1re 1
2 0lt1 0 < 1
3 1 2 elrpii 1 +