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

Proof

Step	Hyp	Ref	Expression
1		negsub	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+\left(-B\right)=A-B$$
2	1	eqcomd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A-B=A+\left(-B\right)$$
3	2	eqeq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A+B=A-B\leftrightarrow A+B=A+\left(-B\right)\right)$$
4		negcl	$$⊢B\in ℂ\to -B\in ℂ$$
5	4	adantl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -B\in ℂ$$
6		addcan	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge -B\in ℂ\right)\to \left(A+B=A+\left(-B\right)\leftrightarrow B=-B\right)$$
7	5 6	mpd3an3	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A+B=A+\left(-B\right)\leftrightarrow B=-B\right)$$
8		eqneg	$$⊢B\in ℂ\to \left(B=-B\leftrightarrow B=0\right)$$
9	8	adantl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(B=-B\leftrightarrow B=0\right)$$
10	3 7 9	3bitrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A+B=A-B\leftrightarrow B=0\right)$$