fzofzp1b

Description: If a point is in a half-open range, the next point is in the closed range. (Contributed by Mario Carneiro, 27-Sep-2015)

		Ref	Expression
	Assertion	fzofzp1b	$⊢ C \in ℤ_{\geq A} \to (C \in (A ..^B) \leftrightarrow C + 1 \in (A \dots B))$

Step	Hyp	Ref	Expression
1		fzofzp1	$⊢ C \in (A ..^B) \to C + 1 \in (A \dots B)$
2		simpl	$⊢ (C \in ℤ_{\geq A} \land C + 1 \in (A \dots B)) \to C \in ℤ_{\geq A}$
3		eluzelz	$⊢ C \in ℤ_{\geq A} \to C \in ℤ$
4		elfzuz3	$⊢ C + 1 \in (A \dots B) \to B \in ℤ_{\geq (C + 1)}$
5		eluzp1m1	$⊢ (C \in ℤ \land B \in ℤ_{\geq (C + 1)}) \to B - 1 \in ℤ_{\geq C}$
6	3 4 5	syl2an	$⊢ (C \in ℤ_{\geq A} \land C + 1 \in (A \dots B)) \to B - 1 \in ℤ_{\geq C}$
7		elfzuzb	$⊢ C \in (A \dots B - 1) \leftrightarrow (C \in ℤ_{\geq A} \land B - 1 \in ℤ_{\geq C})$
8	2 6 7	sylanbrc	$⊢ (C \in ℤ_{\geq A} \land C + 1 \in (A \dots B)) \to C \in (A \dots B - 1)$
9		elfzel2	$⊢ C + 1 \in (A \dots B) \to B \in ℤ$
10	9	adantl	$⊢ (C \in ℤ_{\geq A} \land C + 1 \in (A \dots B)) \to B \in ℤ$
11		fzoval	$⊢ B \in ℤ \to (A ..^B) = (A \dots B - 1)$
12	10 11	syl	$⊢ (C \in ℤ_{\geq A} \land C + 1 \in (A \dots B)) \to (A ..^B) = (A \dots B - 1)$
13	8 12	eleqtrrd	$⊢ (C \in ℤ_{\geq A} \land C + 1 \in (A \dots B)) \to C \in (A ..^B)$
14	13	ex	$⊢ C \in ℤ_{\geq A} \to (C + 1 \in (A \dots B) \to C \in (A ..^B))$
15	1 14	impbid2	$⊢ C \in ℤ_{\geq A} \to (C \in (A ..^B) \leftrightarrow C + 1 \in (A \dots B))$

Metamath Proof Explorer