This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐼 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 ≤ 𝐼 ∧ 𝐼 < ( 𝐴 + 1 ) ) → 𝐼 = 𝐴 ) )

Proof

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