This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )