Theorem subge0

Description: Nonnegative subtraction. (Contributed by NM, 14-Mar-2005) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		0red	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to 0\in ℝ$$
2		simpr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℝ$$
3		simpl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\in ℝ$$
4		leaddsub	$$⊢\left(0\in ℝ\wedge B\in ℝ\wedge A\in ℝ\right)\to \left(0+B\le A\leftrightarrow 0\le A-B\right)$$
5	1 2 3 4	syl3anc	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0+B\le A\leftrightarrow 0\le A-B\right)$$
6	2	recnd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℂ$$
7	6	addlidd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to 0+B=B$$
8	7	breq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0+B\le A\leftrightarrow B\le A\right)$$
9	5 8	bitr3d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0\le A-B\leftrightarrow B\le A\right)$$