Description: One-half is not negative. (Contributed by AV, 7-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | halfge0 | ⊢ 0 ≤ ( 1 / 2 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re | ⊢ 0 ∈ ℝ | |
2 | halfre | ⊢ ( 1 / 2 ) ∈ ℝ | |
3 | halfgt0 | ⊢ 0 < ( 1 / 2 ) | |
4 | 1 2 3 | ltleii | ⊢ 0 ≤ ( 1 / 2 ) |