Theorem xadd0ge

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	xadd0ge.a	|- ( ph -> A e. RR* )
	xadd0ge.b	|- ( ph -> B e. ( 0 [,] +oo ) )
Assertion	xadd0ge	|- ( ph -> A <_ ( A +e B ) )

Proof

Step	Hyp	Ref	Expression
1		xadd0ge.a	|- ( ph -> A e. RR* )
2		xadd0ge.b	|- ( ph -> B e. ( 0 [,] +oo ) )
3		xaddrid	|- ( A e. RR* -> ( A +e 0 ) = A )
4	1 3	syl	|- ( ph -> ( A +e 0 ) = A )
5	4	eqcomd	|- ( ph -> A = ( A +e 0 ) )
6		0xr	|- 0 e. RR*
7	6	a1i	|- ( ph -> 0 e. RR* )
8	1 7	jca	|- ( ph -> ( A e. RR* /\ 0 e. RR* ) )
9		iccssxr	|- ( 0 [,] +oo ) C_ RR*
10	9 2	sselid	|- ( ph -> B e. RR* )
11	1 10	jca	|- ( ph -> ( A e. RR* /\ B e. RR* ) )
12	8 11	jca	|- ( ph -> ( ( A e. RR* /\ 0 e. RR* ) /\ ( A e. RR* /\ B e. RR* ) ) )
13	1	xrleidd	|- ( ph -> A <_ A )
14		pnfxr	|- +oo e. RR*
15	14	a1i	|- ( ph -> +oo e. RR* )
16		iccgelb	|- ( ( 0 e. RR* /\ +oo e. RR* /\ B e. ( 0 [,] +oo ) ) -> 0 <_ B )
17	7 15 2 16	syl3anc	|- ( ph -> 0 <_ B )
18	13 17	jca	|- ( ph -> ( A <_ A /\ 0 <_ B ) )
19		xle2add	|- ( ( ( A e. RR* /\ 0 e. RR* ) /\ ( A e. RR* /\ B e. RR* ) ) -> ( ( A <_ A /\ 0 <_ B ) -> ( A +e 0 ) <_ ( A +e B ) ) )
20	12 18 19	sylc	|- ( ph -> ( A +e 0 ) <_ ( A +e B ) )
21	5 20	eqbrtrd	|- ( ph -> A <_ ( A +e B ) )