Theorem negdi2

Description: Distribution of negative over addition. (Contributed by NM, 1-Jan-2006)

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

Proof

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