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 ) ) → 𝐼 = 𝐴 ) )