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	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) = ( A - B ) <-> B = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		negsub	|- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
2	1	eqcomd	|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) = ( A + -u B ) )
3	2	eqeq2d	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) = ( A - B ) <-> ( A + B ) = ( A + -u B ) ) )
4		negcl	|- ( B e. CC -> -u B e. CC )
5	4	adantl	|- ( ( A e. CC /\ B e. CC ) -> -u B e. CC )
6		addcan	|- ( ( A e. CC /\ B e. CC /\ -u B e. CC ) -> ( ( A + B ) = ( A + -u B ) <-> B = -u B ) )
7	5 6	mpd3an3	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) = ( A + -u B ) <-> B = -u B ) )
8		eqneg	|- ( B e. CC -> ( B = -u B <-> B = 0 ) )
9	8	adantl	|- ( ( A e. CC /\ B e. CC ) -> ( B = -u B <-> B = 0 ) )
10	3 7 9	3bitrd	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) = ( A - B ) <-> B = 0 ) )