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	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A+B=0\leftrightarrow A=-B\right)$$

Proof

Step	Hyp	Ref	Expression
1		0cnd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 0\in ℂ$$
2		simpr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B\in ℂ$$
3		simpl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\in ℂ$$
4	1 2 3	subadd2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(0-B=A\leftrightarrow A+B=0\right)$$
5		df-neg	$$⊢-B=0-B$$
6	5	eqeq1i	$$⊢-B=A\leftrightarrow 0-B=A$$
7		eqcom	$$⊢-B=A\leftrightarrow A=-B$$
8	6 7	bitr3i	$$⊢0-B=A\leftrightarrow A=-B$$
9	4 8	bitr3di	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A+B=0\leftrightarrow A=-B\right)$$