Metamath Proof Explorer


Theorem elrp

Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007)

Ref Expression
Assertion elrp A + A 0 < A

Proof

Step Hyp Ref Expression
1 breq2 x = A 0 < x 0 < A
2 df-rp + = x | 0 < x
3 1 2 elrab2 A + A 0 < A