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

Proof

Step	Hyp	Ref	Expression
1		xadd0ge2.a	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xadd0ge2.b	$$⊢\phi \to B\in \left[0,\mathrm{+\infty }\right]$$
3	1 2	xadd0ge	$$⊢\phi \to A\le A{+}_{𝑒}B$$
4		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
5	4 2	sselid	$$⊢\phi \to B\in {ℝ}^{*}$$
6	1 5	xaddcomd	$$⊢\phi \to A{+}_{𝑒}B=B{+}_{𝑒}A$$
7	3 6	breqtrd	$$⊢\phi \to A\le B{+}_{𝑒}A$$