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

Proof

Step	Hyp	Ref	Expression
1		0cnd	|- ( ( A e. CC /\ B e. CC ) -> 0 e. CC )
2		simpr	|- ( ( A e. CC /\ B e. CC ) -> B e. CC )
3		simpl	|- ( ( A e. CC /\ B e. CC ) -> A e. CC )
4	1 2 3	subadd2d	|- ( ( A e. CC /\ B e. CC ) -> ( ( 0 - B ) = A <-> ( A + B ) = 0 ) )
5		df-neg	|- -u B = ( 0 - B )
6	5	eqeq1i	|- ( -u B = A <-> ( 0 - B ) = A )
7		eqcom	|- ( -u B = A <-> A = -u B )
8	6 7	bitr3i	|- ( ( 0 - B ) = A <-> A = -u B )
9	4 8	bitr3di	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) = 0 <-> A = -u B ) )