Metamath Proof Explorer


Theorem 2rp

Description: 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Assertion 2rp 2 +

Proof

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