Description: A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | ltm1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0lt1 | ||
2 | 0re | ||
3 | 1re | ||
4 | ltsub2 | ||
5 | 2 3 4 | mp3an12 | |
6 | 1 5 | mpbii | |
7 | recn | ||
8 | 7 | subid1d | |
9 | 6 8 | breqtrd |