Metamath Proof Explorer

Theorem negicn

Description: -u _i is a complex number. (Contributed by David A. Wheeler, 7-Dec-2018)

Ref Expression
Assertion negicn 
|- -u _i e. CC

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 negcl 
 |-  ( _i e. CC -> -u _i e. CC )
3 1 2 ax-mp 
 |-  -u _i e. CC