Description: Alternate proof of 0nnn , which requires ax-pre-mulgt0 but is not based on nnne0 (and which can therefore be used in nnne0ALT ). (Contributed by NM, 25-Aug-1999) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0nnnALT | |- -. 0 e. NN |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0lt1 | |- 0 < 1 |
|
| 2 | nnnlt1 | |- ( 0 e. NN -> -. 0 < 1 ) |
|
| 3 | 1 2 | mt2 | |- -. 0 e. NN |