Theorem halflt1

Description: One-half is less than one. (Contributed by NM, 24-Feb-2005)

	Ref	Expression
Assertion	halflt1	$$⊢\frac{1}{2}<1$$

Proof

Step	Hyp	Ref	Expression
1		1div1e1	$$⊢\frac{1}{1}=1$$
2		1lt2	$$⊢1<2$$
3	1 2	eqbrtri	$$⊢\frac{1}{1}<2$$
4		1re	$$⊢1\in ℝ$$
5		2re	$$⊢2\in ℝ$$
6		0lt1	$$⊢0<1$$
7		2pos	$$⊢0<2$$
8	4 4 5 6 7	ltdiv23ii	$$⊢\frac{1}{1}<2\leftrightarrow \frac{1}{2}<1$$
9	3 8	mpbi	$$⊢\frac{1}{2}<1$$