Database
REAL AND COMPLEX NUMBERS
Elementary real and complex functions
Real and imaginary parts; conjugate
re1
Next ⟩
im1
Metamath Proof Explorer
Ascii
Unicode
Theorem
re1
Description:
The real part of one.
(Contributed by
Scott Fenton
, 9-Jun-2006)
Ref
Expression
Assertion
re1
⊢
ℜ
⁡
1
=
1
Proof
Step
Hyp
Ref
Expression
1
1re
⊢
1
∈
ℝ
2
rere
⊢
1
∈
ℝ
→
ℜ
⁡
1
=
1
3
1
2
ax-mp
⊢
ℜ
⁡
1
=
1