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 e. RR |
|
| 2 | ax-1ne0 | |- 1 =/= 0 |
|
| 3 | msqgt0 | |- ( ( 1 e. RR /\ 1 =/= 0 ) -> 0 < ( 1 x. 1 ) ) |
|
| 4 | 1 2 3 | mp2an | |- 0 < ( 1 x. 1 ) |
| 5 | ax-1cn | |- 1 e. CC |
|
| 6 | 5 | mulridi | |- ( 1 x. 1 ) = 1 |
| 7 | 4 6 | breqtri | |- 0 < 1 |