Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
halfre
Next ⟩
halfcn
Metamath Proof Explorer
Ascii
Unicode
Theorem
halfre
Description:
One-half is real.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
halfre
⊢
1
2
∈
ℝ
Proof
Step
Hyp
Ref
Expression
1
2re
⊢
2
∈
ℝ
2
2ne0
⊢
2
≠
0
3
1
2
rereccli
⊢
1
2
∈
ℝ