Description: 0 is less than 1. Theorem I.21 of Apostol p. 20. (Contributed by NM, 17-Jan-1997)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0lt1 | ⊢ 0 < 1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1re | ⊢ 1 ∈ ℝ | |
| 2 | ax-1ne0 | ⊢ 1 ≠ 0 | |
| 3 | msqgt0 | ⊢ ( ( 1 ∈ ℝ ∧ 1 ≠ 0 ) → 0 < ( 1 · 1 ) ) | |
| 4 | 1 2 3 | mp2an | ⊢ 0 < ( 1 · 1 ) |
| 5 | ax-1cn | ⊢ 1 ∈ ℂ | |
| 6 | 5 | mulid1i | ⊢ ( 1 · 1 ) = 1 |
| 7 | 4 6 | breqtri | ⊢ 0 < 1 |