Metamath Proof Explorer


Theorem ltm1

Description: A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006)

Ref Expression
Assertion ltm1 AA1<A

Proof

Step Hyp Ref Expression
1 0lt1 0<1
2 0re 0
3 1re 1
4 ltsub2 01A0<1A1<A0
5 2 3 4 mp3an12 A0<1A1<A0
6 1 5 mpbii AA1<A0
7 recn AA
8 7 subid1d AA0=A
9 6 8 breqtrd AA1<A