Theorem sqsubswap

Description: Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013)

	Ref	Expression
Assertion	sqsubswap	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A-B\right)}^2={\left(B-A\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		subcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A-B\in ℂ$$
2		sqneg	$$⊢A-B\in ℂ\to {\left(-\left(A-B\right)\right)}^2={\left(A-B\right)}^2$$
3	1 2	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(-\left(A-B\right)\right)}^2={\left(A-B\right)}^2$$
4		negsubdi2	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -\left(A-B\right)=B-A$$
5	4	oveq1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(-\left(A-B\right)\right)}^2={\left(B-A\right)}^2$$
6	3 5	eqtr3d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A-B\right)}^2={\left(B-A\right)}^2$$