Metamath Proof Explorer


Theorem elrpd

Description: Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses elrpd.1 φA
elrpd.2 φ0<A
Assertion elrpd φA+

Proof

Step Hyp Ref Expression
1 elrpd.1 φA
2 elrpd.2 φ0<A
3 elrp A+A0<A
4 1 2 3 sylanbrc φA+