# 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 ${⊢}\left({I}\in ℤ\wedge {A}\in ℤ\right)\to \left(\left({A}\le {I}\wedge {I}<{A}+1\right)\to {I}={A}\right)$

### Proof

Step Hyp Ref Expression
1 simprr ${⊢}\left(\left({I}\in ℤ\wedge {A}\in ℤ\right)\wedge \left({A}\le {I}\wedge {I}<{A}+1\right)\right)\to {I}<{A}+1$
2 zleltp1 ${⊢}\left({I}\in ℤ\wedge {A}\in ℤ\right)\to \left({I}\le {A}↔{I}<{A}+1\right)$
3 2 adantr ${⊢}\left(\left({I}\in ℤ\wedge {A}\in ℤ\right)\wedge \left({A}\le {I}\wedge {I}<{A}+1\right)\right)\to \left({I}\le {A}↔{I}<{A}+1\right)$
4 1 3 mpbird ${⊢}\left(\left({I}\in ℤ\wedge {A}\in ℤ\right)\wedge \left({A}\le {I}\wedge {I}<{A}+1\right)\right)\to {I}\le {A}$
5 simprl ${⊢}\left(\left({I}\in ℤ\wedge {A}\in ℤ\right)\wedge \left({A}\le {I}\wedge {I}<{A}+1\right)\right)\to {A}\le {I}$
6 zre ${⊢}{I}\in ℤ\to {I}\in ℝ$
7 zre ${⊢}{A}\in ℤ\to {A}\in ℝ$
8 letri3 ${⊢}\left({I}\in ℝ\wedge {A}\in ℝ\right)\to \left({I}={A}↔\left({I}\le {A}\wedge {A}\le {I}\right)\right)$
9 6 7 8 syl2an ${⊢}\left({I}\in ℤ\wedge {A}\in ℤ\right)\to \left({I}={A}↔\left({I}\le {A}\wedge {A}\le {I}\right)\right)$
10 9 adantr ${⊢}\left(\left({I}\in ℤ\wedge {A}\in ℤ\right)\wedge \left({A}\le {I}\wedge {I}<{A}+1\right)\right)\to \left({I}={A}↔\left({I}\le {A}\wedge {A}\le {I}\right)\right)$
11 4 5 10 mpbir2and ${⊢}\left(\left({I}\in ℤ\wedge {A}\in ℤ\right)\wedge \left({A}\le {I}\wedge {I}<{A}+1\right)\right)\to {I}={A}$
12 11 ex ${⊢}\left({I}\in ℤ\wedge {A}\in ℤ\right)\to \left(\left({A}\le {I}\wedge {I}<{A}+1\right)\to {I}={A}\right)$