This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ ℜ = (x \in ℂ ⟼ \frac{x + \overline{x}}{2})$

Detailed syntax breakdown

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