Metamath Proof Explorer

Theorem negid

Description: Addition of a number and its negative. (Contributed by NM, 14-Mar-2005)

Ref Expression
Assertion negid 
|- ( A e. CC -> ( A + -u A ) = 0 )

Proof

Step Hyp Ref Expression
1 df-neg 
 |-  -u A = ( 0 - A )
2 1 oveq2i 
 |-  ( A + -u A ) = ( A + ( 0 - A ) )
3 0cn 
 |-  0 e. CC
4 pncan3 
 |-  ( ( A e. CC /\ 0 e. CC ) -> ( A + ( 0 - A ) ) = 0 )
5 3 4 mpan2 
 |-  ( A e. CC -> ( A + ( 0 - A ) ) = 0 )
6 2 5 eqtrid 
 |-  ( A e. CC -> ( A + -u A ) = 0 )