Theorem elfzod

Description: Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	elfzod.1	$$⊢\phi \to K\in {\mathbb{Z}}_{\ge M}$$
	elfzod.2	$$⊢\phi \to N\in \mathbb{Z}$$
	elfzod.3	$$⊢\phi \to K<N$$
Assertion	elfzod	$$⊢\phi \to K\in \left(M..^N\right)$$

Proof

Step	Hyp	Ref	Expression
1		elfzod.1	$$⊢\phi \to K\in {\mathbb{Z}}_{\ge M}$$
2		elfzod.2	$$⊢\phi \to N\in \mathbb{Z}$$
3		elfzod.3	$$⊢\phi \to K<N$$
4		elfzo2	$$⊢K\in \left(M..^N\right)\leftrightarrow \left(K\in {\mathbb{Z}}_{\ge M}\wedge N\in \mathbb{Z}\wedge K<N\right)$$
5	1 2 3 4	syl3anbrc	$$⊢\phi \to K\in \left(M..^N\right)$$