Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0lt1 | Structured version Visualization version GIF version |
Description: 0 is less than 1. Theorem I.21 of [Apostol] p. 20. (Contributed by NM, 17-Jan-1997.) |
Ref | Expression |
---|---|
0lt1 | ⊢ 0 < 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 10722 | . . 3 ⊢ 1 ∈ ℝ | |
2 | ax-1ne0 10687 | . . 3 ⊢ 1 ≠ 0 | |
3 | msqgt0 11241 | . . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1)) | |
4 | 1, 2, 3 | mp2an 692 | . 2 ⊢ 0 < (1 · 1) |
5 | ax-1cn 10676 | . . 3 ⊢ 1 ∈ ℂ | |
6 | 5 | mulid1i 10726 | . 2 ⊢ (1 · 1) = 1 |
7 | 4, 6 | breqtri 5056 | 1 ⊢ 0 < 1 |
Copyright terms: Public domain | W3C validator |