Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 simprr ⊢ I ∈ ℤ ∧ A ∈ ℤ ∧ A − 1 < I ∧ I ≤ A → I ≤ A
2 zlem1lt ⊢ A ∈ ℤ ∧ I ∈ ℤ → A ≤ I ↔ A − 1 < I
3 2 ancoms ⊢ I ∈ ℤ ∧ A ∈ ℤ → A ≤ I ↔ A − 1 < I
4 3 biimprcd ⊢ A − 1 < I → I ∈ ℤ ∧ A ∈ ℤ → A ≤ I
5 4 adantr ⊢ A − 1 < I ∧ I ≤ A → I ∈ ℤ ∧ A ∈ ℤ → A ≤ I
6 5 impcom ⊢ I ∈ ℤ ∧ A ∈ ℤ ∧ A − 1 < I ∧ I ≤ A → A ≤ I
7 zre ⊢ I ∈ ℤ → I ∈ ℝ
8 zre ⊢ A ∈ ℤ → A ∈ ℝ
9 letri3 ⊢ I ∈ ℝ ∧ A ∈ ℝ → I = A ↔ I ≤ A ∧ A ≤ I
10 7 8 9 syl2an ⊢ I ∈ ℤ ∧ A ∈ ℤ → I = A ↔ I ≤ A ∧ A ≤ I
11 10 adantr ⊢ I ∈ ℤ ∧ A ∈ ℤ ∧ A − 1 < I ∧ I ≤ A → I = A ↔ I ≤ A ∧ A ≤ I
12 1 6 11 mpbir2and ⊢ I ∈ ℤ ∧ A ∈ ℤ ∧ A − 1 < I ∧ I ≤ A → I = A
13 12 ex ⊢ I ∈ ℤ ∧ A ∈ ℤ → A − 1 < I ∧ I ≤ A → I = A