This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℂ ⟼ ℜ (\frac{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 \div$
6		ci	$class i$
7	4 6 5	co	$class (\frac{x}{i})$
8	7 3	cfv	$class ℜ (\frac{x}{i})$
9	1 2 8	cmpt	$class (x \in ℂ ⟼ ℜ (\frac{x}{i}))$
10	0 9	wceq	$wff ℑ = (x \in ℂ ⟼ ℜ (\frac{x}{i}))$