Theorem negsubdii

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

	Ref	Expression
Hypotheses	negidi.1	$$⊢A\in ℂ$$
	pncan3i.2	$$⊢B\in ℂ$$
Assertion	negsubdii	$$⊢-\left(A-B\right)=-A+B$$

Proof

Step	Hyp	Ref	Expression
1		negidi.1	$$⊢A\in ℂ$$
2		pncan3i.2	$$⊢B\in ℂ$$
3	2	negcli	$$⊢-B\in ℂ$$
4	1 3	negdii	$$⊢-\left(A+\left(-B\right)\right)=-A+\left(-\left(-B\right)\right)$$
5	1 2	negsubi	$$⊢A+\left(-B\right)=A-B$$
6	5	negeqi	$$⊢-\left(A+\left(-B\right)\right)=-\left(A-B\right)$$
7	2	negnegi	$$⊢-\left(-B\right)=B$$
8	7	oveq2i	$$⊢-A+\left(-\left(-B\right)\right)=-A+B$$
9	4 6 8	3eqtr3i	$$⊢-\left(A-B\right)=-A+B$$