Description: The number 8 is positive. (Contributed by NM, 27-May-1999)
Ref | Expression | ||
---|---|---|---|
Assertion | 8pos | ⊢ 0 < 8 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 7re | ⊢ 7 ∈ ℝ | |
2 | 1re | ⊢ 1 ∈ ℝ | |
3 | 7pos | ⊢ 0 < 7 | |
4 | 0lt1 | ⊢ 0 < 1 | |
5 | 1 2 3 4 | addgt0ii | ⊢ 0 < ( 7 + 1 ) |
6 | df-8 | ⊢ 8 = ( 7 + 1 ) | |
7 | 5 6 | breqtrri | ⊢ 0 < 8 |