Metamath Proof Explorer

Theorem addsubeq0

Description: The sum of two complex numbers is equal to the difference of these two complex numbers iff the subtrahend is 0. (Contributed by AV, 8-May-2023)

Ref Expression
Assertion addsubeq0 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = A − B ↔ B = 0

Proof

Step Hyp Ref Expression
1 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
2 1 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B = A + − B
3 2 eqeq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = A − B ↔ A + B = A + − B
4 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
5 4 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → − B ∈ ℂ
6 addcan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ − B ∈ ℂ → A + B = A + − B ↔ B = − B
7 5 6 mpd3an3 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = A + − B ↔ B = − B
8 eqneg ⊢ B ∈ ℂ → B = − B ↔ B = 0
9 8 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → B = − B ↔ B = 0
10 3 7 9 3bitrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = A − B ↔ B = 0