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 e. RR* /\ B e. ( 0 [,] +oo ) ) -> A <_ ( A +e B ) )

Proof

Step	Hyp	Ref	Expression
1		elxrge0	|- ( B e. ( 0 [,] +oo ) <-> ( B e. RR* /\ 0 <_ B ) )
2	1	biimpi	|- ( B e. ( 0 [,] +oo ) -> ( B e. RR* /\ 0 <_ B ) )
3		xraddge02	|- ( ( A e. RR* /\ B e. RR* ) -> ( 0 <_ B -> A <_ ( A +e B ) ) )
4	3	impr	|- ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) ) -> A <_ ( A +e B ) )
5	2 4	sylan2	|- ( ( A e. RR* /\ B e. ( 0 [,] +oo ) ) -> A <_ ( A +e B ) )