Theorem negsubdi

Description: Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		subsub	$$⊢\left(0\in ℂ\wedge A\in ℂ\wedge B\in ℂ\right)\to 0-\left(A-B\right)=0-A+B$$
3	1 2	mp3an1	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 0-\left(A-B\right)=0-A+B$$
4		df-neg	$$⊢-\left(A-B\right)=0-\left(A-B\right)$$
5		df-neg	$$⊢-A=0-A$$
6	5	oveq1i	$$⊢-A+B=0-A+B$$
7	3 4 6	3eqtr4g	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -\left(A-B\right)=-A+B$$