Definition df-re 12933

Description: Define a function whose value is the real part of a complex number. See reval 12939 for its value, recli 13000 for its closure, and replim 12949 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 12930	. 2
2		vx	. . 3
3		cc 9511	. . 3
4	2	cv 1394	. . . . 5
5		ccj 12929	. . . . . 6
6	4, 5	cfv 5593	. . . . 5
7		caddc 9516	. . . . 5
8	4, 6, 7	co 6296	. . . 4
9		c2 10610	. . . 4
10		cdiv 10231	. . . 4
11	8, 9, 10	co 6296	. . 3
12	2, 3, 11	cmpt 4510	. 2
13	1, 12	wceq 1395	1

This definition is referenced by:  reval  12939  ref  12945  cnre2csqima  27893