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 ) ) ) |
| 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 ) ) ) |