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