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	$$⊢\phi \to A\in {ℝ}^{*}$$
	xadd0ge.b	$$⊢\phi \to B\in \left[0,\mathrm{+\infty }\right]$$
Assertion	xadd0ge	$$⊢\phi \to A\le A{+}_{𝑒}B$$

Proof

Step	Hyp	Ref	Expression
1		xadd0ge.a	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xadd0ge.b	$$⊢\phi \to B\in \left[0,\mathrm{+\infty }\right]$$
3		xaddrid	$$⊢A\in {ℝ}^{*}\to A{+}_{𝑒}0=A$$
4	1 3	syl	$$⊢\phi \to A{+}_{𝑒}0=A$$
5	4	eqcomd	$$⊢\phi \to A=A{+}_{𝑒}0$$
6		0xr	$$⊢0\in {ℝ}^{*}$$
7	6	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
8	1 7	jca	$$⊢\phi \to \left(A\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)$$
9		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
10	9 2	sselid	$$⊢\phi \to B\in {ℝ}^{*}$$
11	1 10	jca	$$⊢\phi \to \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)$$
12	8 11	jca	$$⊢\phi \to \left(\left(A\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\wedge \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\right)$$
13	1	xrleidd	$$⊢\phi \to A\le A$$
14		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
15	14	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
16		iccgelb	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge B\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le B$$
17	7 15 2 16	syl3anc	$$⊢\phi \to 0\le B$$
18	13 17	jca	$$⊢\phi \to \left(A\le A\wedge 0\le B\right)$$
19		xle2add	$$⊢\left(\left(A\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\wedge \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\right)\to \left(\left(A\le A\wedge 0\le B\right)\to A{+}_{𝑒}0\le A{+}_{𝑒}B\right)$$
20	12 18 19	sylc	$$⊢\phi \to A{+}_{𝑒}0\le A{+}_{𝑒}B$$
21	5 20	eqbrtrd	$$⊢\phi \to A\le A{+}_{𝑒}B$$