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 e. RR -> ( A - 1 ) < A )

Proof

Step Hyp Ref Expression
1 0lt1
 |-  0 < 1
2 0re
 |-  0 e. RR
3 1re
 |-  1 e. RR
4 ltsub2
 |-  ( ( 0 e. RR /\ 1 e. RR /\ A e. RR ) -> ( 0 < 1 <-> ( A - 1 ) < ( A - 0 ) ) )
5 2 3 4 mp3an12
 |-  ( A e. RR -> ( 0 < 1 <-> ( A - 1 ) < ( A - 0 ) ) )
6 1 5 mpbii
 |-  ( A e. RR -> ( A - 1 ) < ( A - 0 ) )
7 recn
 |-  ( A e. RR -> A e. CC )
8 7 subid1d
 |-  ( A e. RR -> ( A - 0 ) = A )
9 6 8 breqtrd
 |-  ( A e. RR -> ( A - 1 ) < A )