Metamath Proof Explorer


Theorem zgeltp1eq

Description: If an integer is between another integer and its successor, the integer is equal to the other integer. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion zgeltp1eq IAAII<A+1I=A

Proof

Step Hyp Ref Expression
1 simprr IAAII<A+1I<A+1
2 zleltp1 IAIAI<A+1
3 2 adantr IAAII<A+1IAI<A+1
4 1 3 mpbird IAAII<A+1IA
5 simprl IAAII<A+1AI
6 zre II
7 zre AA
8 letri3 IAI=AIAAI
9 6 7 8 syl2an IAI=AIAAI
10 9 adantr IAAII<A+1I=AIAAI
11 4 5 10 mpbir2and IAAII<A+1I=A
12 11 ex IAAII<A+1I=A