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 = x x i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cim class
1 vx setvar x
2 cc class
3 cre class
4 1 cv setvar x
5 cdiv class ÷
6 ci class i
7 4 6 5 co class x i
8 7 3 cfv class x i
9 1 2 8 cmpt class x x i
10 0 9 wceq wff = x x i