Metamath Proof Explorer

Theorem negcl

Description: Closure law for negative. (Contributed by NM, 6-Aug-2003)

Ref Expression
Assertion negcl 
|- ( A e. CC -> -u A e. CC )

Proof

Step Hyp Ref Expression
1 df-neg 
 |-  -u A = ( 0 - A )
2 0cn 
 |-  0 e. CC
3 subcl 
 |-  ( ( 0 e. CC /\ A e. CC ) -> ( 0 - A ) e. CC )
4 2 3 mpan 
 |-  ( A e. CC -> ( 0 - A ) e. CC )
5 1 4 eqeltrid 
 |-  ( A e. CC -> -u A e. CC )