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 e. RR
5		2re	|- 2 e. RR
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