Definition df-re 12436

Description: Define a function whose value is the real part of a complex number. See reval 12442 for its value, recli 12503 for its closure, and replim 12452 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 12433	. 2
2		vx	. . 3
3		cc 9159	. . 3
4	2	cv 1669	. . . . 5
5		ccj 12432	. . . . . 6
6	4, 5	cfv 5438	. . . . 5
7		caddc 9164	. . . . 5
8	4, 6, 7	co 6103	. . . 4
9		c2 10237	. . . 4
10		cdiv 9864	. . . 4
11	8, 9, 10	co 6103	. . 3
12	2, 3, 11	cmpt 4376	. 2
13	1, 12	wceq 1670	1

This definition is referenced by:  reval  12442  ref  12448  cnre2csqima  25520