This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) = ( 𝐴 − 𝐵 ) ↔ 𝐵 = 0 ) )

Proof

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