Theorem halfge0

Description: One-half is not negative. (Contributed by AV, 7-Jun-2020)

	Ref	Expression
Assertion	halfge0	⊢ 0 ≤ ( 1 / 2 )

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		halfre	⊢ ( 1 / 2 ) ∈ ℝ
3		halfgt0	⊢ 0 < ( 1 / 2 )
4	1 2 3	ltleii	⊢ 0 ≤ ( 1 / 2 )