Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
halfgt0
Next ⟩
halfge0
Metamath Proof Explorer
Ascii
Structured
Theorem
halfgt0
Description:
One-half is greater than zero.
(Contributed by
NM
, 24-Feb-2005)
Ref
Expression
Assertion
halfgt0
⊢
0 < ( 1 / 2 )
Proof
Step
Hyp
Ref
Expression
1
2re
⊢
2 ∈ ℝ
2
2pos
⊢
0 < 2
3
1
2
recgt0ii
⊢
0 < ( 1 / 2 )