Definition df-re

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

	Ref	Expression
Assertion	df-re	$$⊢\Re =\left(x\in ℂ⟼\frac{x+\bar{x}}{2}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cre	$$class\Re$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3	1	cv	$$setvarx$$
4		caddc	$$class+$$
5		ccj	$$class*$$
6	3 5	cfv	$$class\bar{x}$$
7	3 6 4	co	$$class\left(x+\bar{x}\right)$$
8		cdiv	$$class÷$$
9		c2	$$class2$$
10	7 9 8	co	$$class\left(\frac{x+\bar{x}}{2}\right)$$
11	1 2 10	cmpt	$$class\left(x\in ℂ⟼\frac{x+\bar{x}}{2}\right)$$
12	0 11	wceq	$$wff\Re =\left(x\in ℂ⟼\frac{x+\bar{x}}{2}\right)$$