Theorem abssub

Description: Swapping order of subtraction doesn't change the absolute value. (Contributed by NM, 1-Oct-1999) (Proof shortened by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	abssub	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A-B\right|=\left|B-A\right|$$

Proof

Step	Hyp	Ref	Expression
1		subcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A-B\in ℂ$$
2		absneg	$$⊢A-B\in ℂ\to \left|-\left(A-B\right)\right|=\left|A-B\right|$$
3	1 2	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|-\left(A-B\right)\right|=\left|A-B\right|$$
4		negsubdi2	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -\left(A-B\right)=B-A$$
5	4	fveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|-\left(A-B\right)\right|=\left|B-A\right|$$
6	3 5	eqtr3d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A-B\right|=\left|B-A\right|$$