Theorem xadd0ge2

Description: A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	xadd0ge2.a	|- ( ph -> A e. RR* )
	xadd0ge2.b	|- ( ph -> B e. ( 0 [,] +oo ) )
Assertion	xadd0ge2	|- ( ph -> A <_ ( B +e A ) )

Proof

Step	Hyp	Ref	Expression
1		xadd0ge2.a	|- ( ph -> A e. RR* )
2		xadd0ge2.b	|- ( ph -> B e. ( 0 [,] +oo ) )
3	1 2	xadd0ge	|- ( ph -> A <_ ( A +e B ) )
4		iccssxr	|- ( 0 [,] +oo ) C_ RR*
5	4 2	sselid	|- ( ph -> B e. RR* )
6	1 5	xaddcomd	|- ( ph -> ( A +e B ) = ( B +e A ) )
7	3 6	breqtrd	|- ( ph -> A <_ ( B +e A ) )