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 I A A 1 < I I A I = A

Proof

Step Hyp Ref Expression
1 simprr I A A 1 < I I A I A
2 zlem1lt A I A I A 1 < I
3 2 ancoms I A A I A 1 < I
4 3 biimprcd A 1 < I I A A I
5 4 adantr A 1 < I I A I A A I
6 5 impcom I A A 1 < I I A A I
7 zre I I
8 zre A A
9 letri3 I A I = A I A A I
10 7 8 9 syl2an I A I = A I A A I
11 10 adantr I A A 1 < I I A I = A I A A I
12 1 6 11 mpbir2and I A A 1 < I I A I = A
13 12 ex I A A 1 < I I A I = A