Definition df-re 12375

Description: Define a function whose value is the real part of a complex number. See reval 12381 for its value, recli 12442 for its closure, and replim 12391 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 12372	. 2
2		vx	. . 3
3		cc 9102	. . 3
4	2	cv 1661	. . . . 5
5		ccj 12371	. . . . . 6
6	4, 5	cfv 5417	. . . . 5
7		caddc 9107	. . . . 5
8	4, 6, 7	co 6067	. . . 4
9		c2 10180	. . . 4
10		cdiv 9807	. . . 4
11	8, 9, 10	co 6067	. . 3
12	2, 3, 11	cmpt 4360	. 2
13	1, 12	wceq 1662	1

This definition is referenced by:  reval  12381  ref  12387  cnre2csqima  25011