Metamath Proof Explorer


Theorem rexrp

Description: Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014)

Ref Expression
Assertion rexrp x+φx0<xφ

Proof

Step Hyp Ref Expression
1 elrp x+x0<x
2 1 anbi1i x+φx0<xφ
3 anass x0<xφx0<xφ
4 2 3 bitri x+φx0<xφ
5 4 rexbii2 x+φx0<xφ