Definition df-im 6753

Description: Define a function whose value is the imaginary part of a complex number. See imvalt 6757 for its value, imcl 6767 for its closure, and replimt 6762 for its use in decomposing a complex number.

Assertion

Ref	Expression
df-im	|- Im = {<.x, y>. | (x e. CC /\ y = U.{w e. RR | E.z e. RR x = (z + (i x. w))})}

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Definition df-im

Step	Hyp	Ref	Expression
1		cim 6749	. 2 class Im
2		vx	. . . . . 6 set x
3	2	cv 957	. . . . 5 class x
4		cc 5244	. . . . 5 class CC
5	3, 4	wcel 960	. . . 4 wff x e. CC
6		vy	. . . . . 6 set y
7	6	cv 957	. . . . 5 class y
8		vz	. . . . . . . . . . 11 set z
9	8	cv 957	. . . . . . . . . 10 class z
10		ci 5248	. . . . . . . . . . 11 class i
11		vw	. . . . . . . . . . . 12 set w
12	11	cv 957	. . . . . . . . . . 11 class w
13		cmul 5251	. . . . . . . . . . 11 class x.
14	10, 12, 13	co 3969	. . . . . . . . . 10 class (i x. w)
15		caddc 5249	. . . . . . . . . 10 class +
16	9, 14, 15	co 3969	. . . . . . . . 9 class (z + (i x. w))
17	3, 16	wceq 958	. . . . . . . 8 wff x = (z + (i x. w))
18		cr 5245	. . . . . . . 8 class RR
19	17, 8, 18	wrex 1649	. . . . . . 7 wff E.z e. RR x = (z + (i x. w))
20	19, 11, 18	crab 1651	. . . . . 6 class {w e. RR | E.z e. RR x = (z + (i x. w))}
21	20	cuni 2507	. . . . 5 class U.{w e. RR | E.z e. RR x = (z + (i x. w))}
22	7, 21	wceq 958	. . . 4 wff y = U.{w e. RR | E.z e. RR x = (z + (i x. w))}
23	5, 22	wa 223	. . 3 wff (x e. CC /\ y = U.{w e. RR | E.z e. RR x = (z + (i x. w))})
24	23, 2, 6	copab 2671	. 2 class {<.x, y>. | (x e. CC /\ y = U.{w e. RR | E.z e. RR x = (z + (i x. w))})}
25	1, 24	wceq 958	1 wff Im = {<.x, y>. | (x e. CC /\ y = U.{w e. RR | E.z e. RR x = (z + (i x. w))})}

This definition is referenced by:  imvalt 6757  imf 6761

Copyright terms: Public domain