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 
|- ( ( I e. ZZ /\ A e. ZZ ) -> ( ( A <_ I /\ I < ( A + 1 ) ) -> I = A ) )

Proof

Step Hyp Ref Expression
1 simprr 
 |-  ( ( ( I e. ZZ /\ A e. ZZ ) /\ ( A <_ I /\ I < ( A + 1 ) ) ) -> I < ( A + 1 ) )
2 zleltp1 
 |-  ( ( I e. ZZ /\ A e. ZZ ) -> ( I <_ A <-> I < ( A + 1 ) ) )
3 2 adantr 
 |-  ( ( ( I e. ZZ /\ A e. ZZ ) /\ ( A <_ I /\ I < ( A + 1 ) ) ) -> ( I <_ A <-> I < ( A + 1 ) ) )
4 1 3 mpbird 
 |-  ( ( ( I e. ZZ /\ A e. ZZ ) /\ ( A <_ I /\ I < ( A + 1 ) ) ) -> I <_ A )
5 simprl 
 |-  ( ( ( I e. ZZ /\ A e. ZZ ) /\ ( A <_ I /\ I < ( A + 1 ) ) ) -> A <_ I )
6 zre 
 |-  ( I e. ZZ -> I e. RR )
7 zre 
 |-  ( A e. ZZ -> A e. RR )
8 letri3 
 |-  ( ( I e. RR /\ A e. RR ) -> ( I = A <-> ( I <_ A /\ A <_ I ) ) )
9 6 7 8 syl2an 
 |-  ( ( I e. ZZ /\ A e. ZZ ) -> ( I = A <-> ( I <_ A /\ A <_ I ) ) )
10 9 adantr 
 |-  ( ( ( I e. ZZ /\ A e. ZZ ) /\ ( A <_ I /\ I < ( A + 1 ) ) ) -> ( I = A <-> ( I <_ A /\ A <_ I ) ) )
11 4 5 10 mpbir2and 
 |-  ( ( ( I e. ZZ /\ A e. ZZ ) /\ ( A <_ I /\ I < ( A + 1 ) ) ) -> I = A )
12 11 ex 
 |-  ( ( I e. ZZ /\ A e. ZZ ) -> ( ( A <_ I /\ I < ( A + 1 ) ) -> I = A ) )