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 \in ℤ \land A \in ℤ) \to ((A \leq I \land I < A + 1) \to I = A)$

Proof

Step	Hyp	Ref	Expression
1		simprr	$⊢ ((I \in ℤ \land A \in ℤ) \land (A \leq I \land I < A + 1)) \to I < A + 1$
2		zleltp1	$⊢ (I \in ℤ \land A \in ℤ) \to (I \leq A \leftrightarrow I < A + 1)$
3	2	adantr	$⊢ ((I \in ℤ \land A \in ℤ) \land (A \leq I \land I < A + 1)) \to (I \leq A \leftrightarrow I < A + 1)$
4	1 3	mpbird	$⊢ ((I \in ℤ \land A \in ℤ) \land (A \leq I \land I < A + 1)) \to I \leq A$
5		simprl	$⊢ ((I \in ℤ \land A \in ℤ) \land (A \leq I \land I < A + 1)) \to A \leq I$
6		zre	$⊢ I \in ℤ \to I \in ℝ$
7		zre	$⊢ A \in ℤ \to A \in ℝ$
8		letri3	$⊢ (I \in ℝ \land A \in ℝ) \to (I = A \leftrightarrow (I \leq A \land A \leq I))$
9	6 7 8	syl2an	$⊢ (I \in ℤ \land A \in ℤ) \to (I = A \leftrightarrow (I \leq A \land A \leq I))$
10	9	adantr	$⊢ ((I \in ℤ \land A \in ℤ) \land (A \leq I \land I < A + 1)) \to (I = A \leftrightarrow (I \leq A \land A \leq I))$
11	4 5 10	mpbir2and	$⊢ ((I \in ℤ \land A \in ℤ) \land (A \leq I \land I < A + 1)) \to I = A$
12	11	ex	$⊢ (I \in ℤ \land A \in ℤ) \to ((A \leq I \land I < A + 1) \to I = A)$