Metamath Proof Explorer


Theorem imcl

Description: The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

Ref Expression
Assertion imcl AA

Proof

Step Hyp Ref Expression
1 imre AA=iA
2 negicn i
3 mulcl iAiA
4 2 3 mpan AiA
5 recl iAiA
6 4 5 syl AiA
7 1 6 eqeltrd AA