Theorem elfzofz

Description: A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015)

	Ref	Expression
Assertion	elfzofz	$$⊢K\in \left(M..^N\right)\to K\in \left(M\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		elfzouz	$$⊢K\in \left(M..^N\right)\to K\in {\mathbb{Z}}_{\ge M}$$
2		elfzouz2	$$⊢K\in \left(M..^N\right)\to N\in {\mathbb{Z}}_{\ge K}$$
3		elfzuzb	$$⊢K\in \left(M\dots N\right)\leftrightarrow \left(K\in {\mathbb{Z}}_{\ge M}\wedge N\in {\mathbb{Z}}_{\ge K}\right)$$
4	1 2 3	sylanbrc	$$⊢K\in \left(M..^N\right)\to K\in \left(M\dots N\right)$$