Database
REAL AND COMPLEX NUMBERS
Elementary real and complex functions
Real and imaginary parts; conjugate
re0
Next ⟩
im0
Metamath Proof Explorer
Ascii
Unicode
Theorem
re0
Description:
The real part of zero.
(Contributed by
NM
, 27-Jul-1999)
Ref
Expression
Assertion
re0
⊢
ℜ
⁡
0
=
0
Proof
Step
Hyp
Ref
Expression
1
0re
⊢
0
∈
ℝ
2
rere
⊢
0
∈
ℝ
→
ℜ
⁡
0
=
0
3
1
2
ax-mp
⊢
ℜ
⁡
0
=
0