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 ) |
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 ) |