This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzisfzounsn

Description: A finite interval of integers as union of a half-open integer range and a singleton. (Contributed by Alexander van der Vekens, 15-Jun-2018)

		Ref	Expression
	Assertion	fzisfzounsn	$⊢ B \in ℤ_{\geq A} \to (A \dots B) = (A ..^B) \cup \{B\}$

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$⊢ B \in ℤ_{\geq A} \to B \in ℤ$
2		fzval3	$⊢ B \in ℤ \to (A \dots B) = (A ..^B + 1)$
3	1 2	syl	$⊢ B \in ℤ_{\geq A} \to (A \dots B) = (A ..^B + 1)$
4		fzosplitsn	$⊢ B \in ℤ_{\geq A} \to (A ..^B + 1) = (A ..^B) \cup \{B\}$
5	3 4	eqtrd	$⊢ B \in ℤ_{\geq A} \to (A \dots B) = (A ..^B) \cup \{B\}$