This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Elementary real and complex functions Real and imaginary parts; conjugate df-re
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 ) )