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, 9May1999)
Ref  Expression  

Assertion  dfim   Im = ( x e. CC > ( Re ` ( x / _i ) ) ) 
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 ) ) ) 