Description: If an integer is between another integer and its predecessor, the integer is equal to the other integer. (Contributed by AV, 7-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | zgtp1leeq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprr | |
|
2 | zlem1lt | |
|
3 | 2 | ancoms | |
4 | 3 | biimprcd | |
5 | 4 | adantr | |
6 | 5 | impcom | |
7 | zre | |
|
8 | zre | |
|
9 | letri3 | |
|
10 | 7 8 9 | syl2an | |
11 | 10 | adantr | |
12 | 1 6 11 | mpbir2and | |
13 | 12 | ex | |