Metamath Proof Explorer


Theorem xrge0addge

Description: A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 19-Jul-2020)

Ref Expression
Assertion xrge0addge A*B0+∞AA+𝑒B

Proof

Step Hyp Ref Expression
1 elxrge0 B0+∞B*0B
2 1 biimpi B0+∞B*0B
3 xraddge02 A*B*0BAA+𝑒B
4 3 impr A*B*0BAA+𝑒B
5 2 4 sylan2 A*B0+∞AA+𝑒B