Theorem negdi

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

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

Proof

Step	Hyp	Ref	Expression
1		subneg	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A-\left(-B\right)=A+B$$
2	1	negeqd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -\left(A-\left(-B\right)\right)=-\left(A+B\right)$$
3		negcl	$$⊢B\in ℂ\to -B\in ℂ$$
4		negsubdi	$$⊢\left(A\in ℂ\wedge -B\in ℂ\right)\to -\left(A-\left(-B\right)\right)=-A+\left(-B\right)$$
5	3 4	sylan2	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -\left(A-\left(-B\right)\right)=-A+\left(-B\right)$$
6	2 5	eqtr3d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -\left(A+B\right)=-A+\left(-B\right)$$