Metamath Proof Explorer

Theorem subneg

Description: Relationship between subtraction and negative. (Contributed by NM, 10-May-2004) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion subneg ⊢A∈ℂ∧B∈ℂ→A−−B=A+B

Proof

Step Hyp Ref Expression
1 df-neg ⊢−B=0−B
2 1 oveq2i ⊢A−−B=A−0−B
3 0cn ⊢0∈ℂ
4 subsub ⊢A∈ℂ∧0∈ℂ∧B∈ℂ→A−0−B=A-0+B
5 3 4 mp3an2 ⊢A∈ℂ∧B∈ℂ→A−0−B=A-0+B
6 2 5 eqtrid ⊢A∈ℂ∧B∈ℂ→A−−B=A-0+B
7 subid1 ⊢A∈ℂ→A−0=A
8 7 adantr ⊢A∈ℂ∧B∈ℂ→A−0=A
9 8 oveq1d ⊢A∈ℂ∧B∈ℂ→A-0+B=A+B
10 6 9 eqtrd ⊢A∈ℂ∧B∈ℂ→A−−B=A+B