Theorem negsub

Description: Relationship between subtraction and negative. Theorem I.3 of Apostol p. 18. (Contributed by NM, 21-Jan-1997) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		df-neg	$$⊢-B=0-B$$
2	1	oveq2i	$$⊢A+\left(-B\right)=A+0-B$$
3	2	a1i	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+\left(-B\right)=A+0-B$$
4		0cn	$$⊢0\in ℂ$$
5		addsubass	$$⊢\left(A\in ℂ\wedge 0\in ℂ\wedge B\in ℂ\right)\to A+0-B=A+0-B$$
6	4 5	mp3an2	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+0-B=A+0-B$$
7		simpl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\in ℂ$$
8	7	addid1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+0=A$$
9	8	oveq1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+0-B=A-B$$
10	3 6 9	3eqtr2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+\left(-B\right)=A-B$$