Metamath Proof Explorer

Theorem negnegd

Description: A number is equal to the negative of its negative. Theorem I.4 of Apostol p. 18. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypothesis negidd.1 
|- ( ph -> A e. CC )
Assertion negnegd 
|- ( ph -> -u -u A = A )

Proof

Step Hyp Ref Expression
1 negidd.1 
 |-  ( ph -> A e. CC )
2 negneg 
 |-  ( A e. CC -> -u -u A = A )
3 1 2 syl 
 |-  ( ph -> -u -u A = A )