Theorem xraddge02

Description: A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 28-Dec-2016)

	Ref	Expression
Assertion	xraddge02	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(0\le B\to A\le A{+}_{𝑒}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrleid	$$⊢A\in {ℝ}^{*}\to A\le A$$
2	1	adantr	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to A\le A$$
3		simpl	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to A\in {ℝ}^{*}$$
4		0xr	$$⊢0\in {ℝ}^{*}$$
5	3 4	jctir	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)$$
6		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)$$
7	5 6	mpancom	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\left(A\le A\wedge 0\le B\right)\to A{+}_{𝑒}0\le A{+}_{𝑒}B\right)$$
8	2 7	mpand	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(0\le B\to A{+}_{𝑒}0\le A{+}_{𝑒}B\right)$$
9		xaddrid	$$⊢A\in {ℝ}^{*}\to A{+}_{𝑒}0=A$$
10	9	breq1d	$$⊢A\in {ℝ}^{*}\to \left(A{+}_{𝑒}0\le A{+}_{𝑒}B\leftrightarrow A\le A{+}_{𝑒}B\right)$$
11	10	adantr	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A{+}_{𝑒}0\le A{+}_{𝑒}B\leftrightarrow A\le A{+}_{𝑒}B\right)$$
12	8 11	sylibd	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(0\le B\to A\le A{+}_{𝑒}B\right)$$