Metamath Proof Explorer


Theorem rexrp

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

Ref Expression
Assertion rexrp x + φ x 0 < x φ

Proof

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