This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (M ..^N) \to K \in (M \dots N)$

Step	Hyp	Ref	Expression
1		elfzouz	$⊢ K \in (M ..^N) \to K \in ℤ_{\geq M}$
2		elfzouz2	$⊢ K \in (M ..^N) \to N \in ℤ_{\geq K}$
3		elfzuzb	$⊢ K \in (M \dots N) \leftrightarrow (K \in ℤ_{\geq M} \land N \in ℤ_{\geq K})$
4	1 2 3	sylanbrc	$⊢ K \in (M ..^N) \to K \in (M \dots N)$