Theorem addeq0

Description: Two complex numbers add up to zero iff they are each other's opposites. (Contributed by Thierry Arnoux, 2-May-2017)

	Ref	Expression
Assertion	addeq0	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) = 0 ↔ 𝐴 = - 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		0cnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 0 ∈ ℂ )
2		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
3		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
4	1 2 3	subadd2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 0 − 𝐵 ) = 𝐴 ↔ ( 𝐴 + 𝐵 ) = 0 ) )
5		df-neg	⊢ - 𝐵 = ( 0 − 𝐵 )
6	5	eqeq1i	⊢ ( - 𝐵 = 𝐴 ↔ ( 0 − 𝐵 ) = 𝐴 )
7		eqcom	⊢ ( - 𝐵 = 𝐴 ↔ 𝐴 = - 𝐵 )
8	6 7	bitr3i	⊢ ( ( 0 − 𝐵 ) = 𝐴 ↔ 𝐴 = - 𝐵 )
9	4 8	bitr3di	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) = 0 ↔ 𝐴 = - 𝐵 ) )