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 syl5eq ⊢ 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