Metamath Proof Explorer


Definition df-im

Description: Define a function whose value is the imaginary part of a complex number. See imval for its value, imcli for its closure, and replim for its use in decomposing a complex number. (Contributed by NM, 9-May-1999)

Ref Expression
Assertion df-im
|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cim
 |-  Im
1 vx
 |-  x
2 cc
 |-  CC
3 cre
 |-  Re
4 1 cv
 |-  x
5 cdiv
 |-  /
6 ci
 |-  _i
7 4 6 5 co
 |-  ( x / _i )
8 7 3 cfv
 |-  ( Re ` ( x / _i ) )
9 1 2 8 cmpt
 |-  ( x e. CC |-> ( Re ` ( x / _i ) ) )
10 0 9 wceq
 |-  Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )