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

Proof

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