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

Proof

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