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 {\mathbb{Z}}_{\ge A}\to \left(A\dots B\right)=\left(A..^B\right)\cup \left\{B\right\}$$

Proof

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