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 ∈ ℤ ∧ A ∈ ℤ → A ≤ I ∧ I < A + 1 → I = A

Proof

Step Hyp Ref Expression
1 simprr ⊢ I ∈ ℤ ∧ A ∈ ℤ ∧ A ≤ I ∧ I < A + 1 → I < A + 1
2 zleltp1 ⊢ I ∈ ℤ ∧ A ∈ ℤ → I ≤ A ↔ I < A + 1
3 2 adantr ⊢ I ∈ ℤ ∧ A ∈ ℤ ∧ A ≤ I ∧ I < A + 1 → I ≤ A ↔ I < A + 1
4 1 3 mpbird ⊢ I ∈ ℤ ∧ A ∈ ℤ ∧ A ≤ I ∧ I < A + 1 → I ≤ A
5 simprl ⊢ I ∈ ℤ ∧ A ∈ ℤ ∧ A ≤ I ∧ I < A + 1 → A ≤ I
6 zre ⊢ I ∈ ℤ → I ∈ ℝ
7 zre ⊢ A ∈ ℤ → A ∈ ℝ
8 letri3 ⊢ I ∈ ℝ ∧ A ∈ ℝ → I = A ↔ I ≤ A ∧ A ≤ I
9 6 7 8 syl2an ⊢ I ∈ ℤ ∧ A ∈ ℤ → I = A ↔ I ≤ A ∧ A ≤ I
10 9 adantr ⊢ I ∈ ℤ ∧ A ∈ ℤ ∧ A ≤ I ∧ I < A + 1 → I = A ↔ I ≤ A ∧ A ≤ I
11 4 5 10 mpbir2and ⊢ I ∈ ℤ ∧ A ∈ ℤ ∧ A ≤ I ∧ I < A + 1 → I = A
12 11 ex ⊢ I ∈ ℤ ∧ A ∈ ℤ → A ≤ I ∧ I < A + 1 → I = A