This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem halflt1

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

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

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$