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 ) )