Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
halflt1
Next ⟩
1mhlfehlf
Metamath Proof Explorer
Ascii
Unicode
Theorem
halflt1
Description:
One-half is less than one.
(Contributed by
NM
, 24-Feb-2005)
Ref
Expression
Assertion
halflt1
⊢
1
2
<
1
Proof
Step
Hyp
Ref
Expression
1
1div1e1
⊢
1
1
=
1
2
1lt2
⊢
1
<
2
3
1
2
eqbrtri
⊢
1
1
<
2
4
1re
⊢
1
∈
ℝ
5
2re
⊢
2
∈
ℝ
6
0lt1
⊢
0
<
1
7
2pos
⊢
0
<
2
8
4
4
5
6
7
ltdiv23ii
⊢
1
1
<
2
↔
1
2
<
1
9
3
8
mpbi
⊢
1
2
<
1