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	⊢ ℑ = ( 𝑥 ∈ ℂ ↦ ( ℜ ‘ ( 𝑥 / i ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cim	⊢ ℑ
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		cre	⊢ ℜ
4	1	cv	⊢ 𝑥
5		cdiv	⊢ /
6		ci	⊢ i
7	4 6 5	co	⊢ ( 𝑥 / i )
8	7 3	cfv	⊢ ( ℜ ‘ ( 𝑥 / i ) )
9	1 2 8	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ ( ℜ ‘ ( 𝑥 / i ) ) )
10	0 9	wceq	⊢ ℑ = ( 𝑥 ∈ ℂ ↦ ( ℜ ‘ ( 𝑥 / i ) ) )