Metamath Proof Explorer


Theorem ralrp

Description: Quantification over positive reals. (Contributed by NM, 12-Feb-2008)

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

Proof

Step Hyp Ref Expression
1 elrp x + x 0 < x
2 1 imbi1i x + φ x 0 < x φ
3 impexp x 0 < x φ x 0 < x φ
4 2 3 bitri x + φ x 0 < x φ
5 4 ralbii2 x + φ x 0 < x φ