Metamath Proof Explorer


Theorem zgtp1leeq

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 IAA1<IIAI=A

Proof

Step Hyp Ref Expression
1 simprr IAA1<IIAIA
2 zlem1lt AIAIA1<I
3 2 ancoms IAAIA1<I
4 3 biimprcd A1<IIAAI
5 4 adantr A1<IIAIAAI
6 5 impcom IAA1<IIAAI
7 zre II
8 zre AA
9 letri3 IAI=AIAAI
10 7 8 9 syl2an IAI=AIAAI
11 10 adantr IAA1<IIAI=AIAAI
12 1 6 11 mpbir2and IAA1<IIAI=A
13 12 ex IAA1<IIAI=A