Metamath Proof Explorer


Theorem negicn

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

Ref Expression
Assertion negicn i

Proof

Step Hyp Ref Expression
1 ax-icn i
2 negcl i i
3 1 2 ax-mp i