Definition df-re 12589

Description: Define a function whose value is the real part of a complex number. See reval 12595 for its value, recli 12656 for its closure, and replim 12605 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 12586	. 2
2		vx	. . 3
3		cc 9280	. . 3
4	2	cv 1368	. . . . 5
5		ccj 12585	. . . . . 6
6	4, 5	cfv 5418	. . . . 5
7		caddc 9285	. . . . 5
8	4, 6, 7	co 6091	. . . 4
9		c2 10371	. . . 4
10		cdiv 9993	. . . 4
11	8, 9, 10	co 6091	. . 3
12	2, 3, 11	cmpt 4350	. 2
13	1, 12	wceq 1369	1

This definition is referenced by:  reval  12595  ref  12601  cnre2csqima  26341