Theorem addge01

Description: A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005)

	Ref	Expression
Assertion	addge01	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0\le B\leftrightarrow A\le A+B\right)$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		leadd2	$$⊢\left(0\in ℝ\wedge B\in ℝ\wedge A\in ℝ\right)\to \left(0\le B\leftrightarrow A+0\le A+B\right)$$
3	1 2	mp3an1	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(0\le B\leftrightarrow A+0\le A+B\right)$$
4	3	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0\le B\leftrightarrow A+0\le A+B\right)$$
5		recn	$$⊢A\in ℝ\to A\in ℂ$$
6	5	addridd	$$⊢A\in ℝ\to A+0=A$$
7	6	adantr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+0=A$$
8	7	breq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A+0\le A+B\leftrightarrow A\le A+B\right)$$
9	4 8	bitrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0\le B\leftrightarrow A\le A+B\right)$$