Metamath Proof Explorer


Theorem ltm1

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

Ref Expression
Assertion ltm1 A A 1 < A

Proof

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