Theorem negsubdi2

Description: Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999)

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

Proof

Step	Hyp	Ref	Expression
1		negsubdi	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -\left(A-B\right)=-A+B$$
2		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
3		addcom	$$⊢\left(-A\in ℂ\wedge B\in ℂ\right)\to -A+B=B+\left(-A\right)$$
4	2 3	sylan	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -A+B=B+\left(-A\right)$$
5		negsub	$$⊢\left(B\in ℂ\wedge A\in ℂ\right)\to B+\left(-A\right)=B-A$$
6	5	ancoms	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B+\left(-A\right)=B-A$$
7	1 4 6	3eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -\left(A-B\right)=B-A$$