Metamath Proof Explorer

Theorem negeq0

Description: A number is zero iff its negative is zero. (Contributed by NM, 12-Jul-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion negeq0 
|- ( A e. CC -> ( A = 0 <-> -u A = 0 ) )

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 neg11 
 |-  ( ( A e. CC /\ 0 e. CC ) -> ( -u A = -u 0 <-> A = 0 ) )
3 1 2 mpan2 
 |-  ( A e. CC -> ( -u A = -u 0 <-> A = 0 ) )
4 neg0 
 |-  -u 0 = 0
5 4 eqeq2i 
 |-  ( -u A = -u 0 <-> -u A = 0 )
6 3 5 bitr3di 
 |-  ( A e. CC -> ( A = 0 <-> -u A = 0 ) )