Theorem elfzomin

Description: Membership of an integer in the smallest open range of integers. (Contributed by Alexander van der Vekens, 22-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		snidg	$$⊢Z\in \mathbb{Z}\to Z\in \left\{Z\right\}$$
2		fzosn	$$⊢Z\in \mathbb{Z}\to \left(Z..^Z+1\right)=\left\{Z\right\}$$
3	1 2	eleqtrrd	$$⊢Z\in \mathbb{Z}\to Z\in \left(Z..^Z+1\right)$$