Theorem fzosn

Description: Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015)

	Ref	Expression
Assertion	fzosn	$$⊢A\in \mathbb{Z}\to \left(A..^A+1\right)=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fzval3	$$⊢A\in \mathbb{Z}\to \left(A\dots A\right)=\left(A..^A+1\right)$$
2		fzsn	$$⊢A\in \mathbb{Z}\to \left(A\dots A\right)=\left\{A\right\}$$
3	1 2	eqtr3d	$$⊢A\in \mathbb{Z}\to \left(A..^A+1\right)=\left\{A\right\}$$