Metamath Proof Explorer

Theorem addn0nid

Description: Adding a nonzero number to a complex number does not yield the complex number. (Contributed by AV, 17-Jan-2021)

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

Proof

Step Hyp Ref Expression
1 addid0 
 |-  ( ( X e. CC /\ Y e. CC ) -> ( ( X + Y ) = X <-> Y = 0 ) )
2 1 biimpd 
 |-  ( ( X e. CC /\ Y e. CC ) -> ( ( X + Y ) = X -> Y = 0 ) )
3 2 necon3d 
 |-  ( ( X e. CC /\ Y e. CC ) -> ( Y =/= 0 -> ( X + Y ) =/= X ) )
4 3 3impia 
 |-  ( ( X e. CC /\ Y e. CC /\ Y =/= 0 ) -> ( X + Y ) =/= X )