fzoend

Description: The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015)

		Ref	Expression
	Assertion	fzoend	$⊢ A \in (A ..^B) \to B - 1 \in (A ..^B)$

Step	Hyp	Ref	Expression
1		id	$⊢ A \in (A ..^B) \to A \in (A ..^B)$
2		elfzoel2	$⊢ A \in (A ..^B) \to B \in ℤ$
3		fzoval	$⊢ B \in ℤ \to (A ..^B) = (A \dots B - 1)$
4	2 3	syl	$⊢ A \in (A ..^B) \to (A ..^B) = (A \dots B - 1)$
5	1 4	eleqtrd	$⊢ A \in (A ..^B) \to A \in (A \dots B - 1)$
6		elfzuz3	$⊢ A \in (A \dots B - 1) \to B - 1 \in ℤ_{\geq A}$
7	5 6	syl	$⊢ A \in (A ..^B) \to B - 1 \in ℤ_{\geq A}$
8		eluzfz2	$⊢ B - 1 \in ℤ_{\geq A} \to B - 1 \in (A \dots B - 1)$
9	7 8	syl	$⊢ A \in (A ..^B) \to B - 1 \in (A \dots B - 1)$
10	9 4	eleqtrrd	$⊢ A \in (A ..^B) \to B - 1 \in (A ..^B)$

Metamath Proof Explorer