Metamath Proof Explorer


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