Definition df-re 11956

Description: Define a function whose value is the real part of a complex number. See reval 11962 for its value, recli 12023 for its closure, and replim 11972 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)

Assertion

Ref	Expression
df-re

Detailed syntax breakdown of Definition df-re

Step	Hyp	Ref	Expression
1		cre 11953	. 2
2		vx	. . 3
3		cc 9039	. . 3
4	2	cv 1653	. . . . 5
5		ccj 11952	. . . . . 6
6	4, 5	cfv 5501	. . . . 5
7		caddc 9044	. . . . 5
8	4, 6, 7	co 6129	. . . 4
9		c2 10100	. . . 4
10		cdiv 9728	. . . 4
11	8, 9, 10	co 6129	. . 3
12	2, 3, 11	cmpt 4301	. 2
13	1, 12	wceq 1654	1

This definition is referenced by:  reval  11962  ref  11968  cnre2csqima  24358