Theorem abssuble0

Description: Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008)

	Ref	Expression
Assertion	abssuble0	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left|A-B\right|=B-A$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		recn	$$⊢B\in ℝ\to B\in ℂ$$
3		abssub	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A-B\right|=\left|B-A\right|$$
4	1 2 3	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left|A-B\right|=\left|B-A\right|$$
5	4	3adant3	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left|A-B\right|=\left|B-A\right|$$
6		abssubge0	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left|B-A\right|=B-A$$
7	5 6	eqtrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left|A-B\right|=B-A$$