Metamath Proof Explorer

Theorem uzssico

Description: Upper integer sets are a subset of the corresponding closed-below, open-above intervals. (Contributed by Thierry Arnoux, 29-Dec-2021)

		Ref	Expression
	Assertion	uzssico	$⊢ M \in ℤ \to ℤ_{\geq M} \subseteq [M, +∞)$

Proof

Step	Hyp	Ref	Expression
1		zssre	$⊢ ℤ \subseteq ℝ$
2	1	sseli	$⊢ x \in ℤ \to x \in ℝ$
3	2	a1i	$⊢ M \in ℤ \to (x \in ℤ \to x \in ℝ)$
4	3	anim1d	$⊢ M \in ℤ \to ((x \in ℤ \land M \leq x) \to (x \in ℝ \land M \leq x))$
5		eluz1	$⊢ M \in ℤ \to (x \in ℤ_{\geq M} \leftrightarrow (x \in ℤ \land M \leq x))$
6		zre	$⊢ M \in ℤ \to M \in ℝ$
7		elicopnf	$⊢ M \in ℝ \to (x \in [M, +∞) \leftrightarrow (x \in ℝ \land M \leq x))$
8	6 7	syl	$⊢ M \in ℤ \to (x \in [M, +∞) \leftrightarrow (x \in ℝ \land M \leq x))$
9	4 5 8	3imtr4d	$⊢ M \in ℤ \to (x \in ℤ_{\geq M} \to x \in [M, +∞))$
10	9	ssrdv	$⊢ M \in ℤ \to ℤ_{\geq M} \subseteq [M, +∞)$