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	⊢ ℜ = ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 + ( ∗ ‘ 𝑥 ) ) / 2 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cre	⊢ ℜ
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3	1	cv	⊢ 𝑥
4		caddc	⊢ +
5		ccj	⊢ ∗
6	3 5	cfv	⊢ ( ∗ ‘ 𝑥 )
7	3 6 4	co	⊢ ( 𝑥 + ( ∗ ‘ 𝑥 ) )
8		cdiv	⊢ /
9		c2	⊢ 2
10	7 9 8	co	⊢ ( ( 𝑥 + ( ∗ ‘ 𝑥 ) ) / 2 )
11	1 2 10	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 + ( ∗ ‘ 𝑥 ) ) / 2 ) )
12	0 11	wceq	⊢ ℜ = ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 + ( ∗ ‘ 𝑥 ) ) / 2 ) )