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

Metamath Proof Explorer

Theorem addid0

Description: If adding a number to a another number yields the other number, the added number must be 0 . This shows that 0 is the unique (right) identity of the complex numbers. (Contributed by AV, 17-Jan-2021)

Ref Expression
Assertion addid0 
|- ( ( X e. CC /\ Y e. CC ) -> ( ( X + Y ) = X <-> Y = 0 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( X e. CC /\ Y e. CC ) -> X e. CC )
2 simpr 
 |-  ( ( X e. CC /\ Y e. CC ) -> Y e. CC )
3 1 1 2 subaddd 
 |-  ( ( X e. CC /\ Y e. CC ) -> ( ( X - X ) = Y <-> ( X + Y ) = X ) )
4 eqcom 
 |-  ( ( X - X ) = Y <-> Y = ( X - X ) )
5 simpr 
 |-  ( ( X e. CC /\ Y = ( X - X ) ) -> Y = ( X - X ) )
6 subid 
 |-  ( X e. CC -> ( X - X ) = 0 )
7 6 adantr 
 |-  ( ( X e. CC /\ Y = ( X - X ) ) -> ( X - X ) = 0 )
8 5 7 eqtrd 
 |-  ( ( X e. CC /\ Y = ( X - X ) ) -> Y = 0 )
9 8 ex 
 |-  ( X e. CC -> ( Y = ( X - X ) -> Y = 0 ) )
10 4 9 biimtrid 
 |-  ( X e. CC -> ( ( X - X ) = Y -> Y = 0 ) )
11 10 adantr 
 |-  ( ( X e. CC /\ Y e. CC ) -> ( ( X - X ) = Y -> Y = 0 ) )
12 3 11 sylbird 
 |-  ( ( X e. CC /\ Y e. CC ) -> ( ( X + Y ) = X -> Y = 0 ) )
13 oveq2 
 |-  ( Y = 0 -> ( X + Y ) = ( X + 0 ) )
14 addrid 
 |-  ( X e. CC -> ( X + 0 ) = X )
15 13 14 sylan9eqr 
 |-  ( ( X e. CC /\ Y = 0 ) -> ( X + Y ) = X )
16 15 ex 
 |-  ( X e. CC -> ( Y = 0 -> ( X + Y ) = X ) )
17 16 adantr 
 |-  ( ( X e. CC /\ Y e. CC ) -> ( Y = 0 -> ( X + Y ) = X ) )
18 12 17 impbid 
 |-  ( ( X e. CC /\ Y e. CC ) -> ( ( X + Y ) = X <-> Y = 0 ) )