# Metamath Proof Explorer

## 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}$