Description: A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 2-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | lem1 | |- ( A e. RR -> ( A - 1 ) <_ A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltm1 | |- ( A e. RR -> ( A - 1 ) < A ) |
|
2 | peano2rem | |- ( A e. RR -> ( A - 1 ) e. RR ) |
|
3 | ltle | |- ( ( ( A - 1 ) e. RR /\ A e. RR ) -> ( ( A - 1 ) < A -> ( A - 1 ) <_ A ) ) |
|
4 | 2 3 | mpancom | |- ( A e. RR -> ( ( A - 1 ) < A -> ( A - 1 ) <_ A ) ) |
5 | 1 4 | mpd | |- ( A e. RR -> ( A - 1 ) <_ A ) |