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

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	⊢ ( 𝑀 ∈ ℤ → ( ℤ_≥ ‘ 𝑀 ) ⊆ ( 𝑀 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		zssre	⊢ ℤ ⊆ ℝ
2	1	sseli	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
3	2	a1i	⊢ ( 𝑀 ∈ ℤ → ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ ) )
4	3	anim1d	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) → ( 𝑥 ∈ ℝ ∧ 𝑀 ≤ 𝑥 ) ) )
5		eluz1	⊢ ( 𝑀 ∈ ℤ → ( 𝑥 ∈ ( ℤ_≥ ‘ 𝑀 ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) )
6		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
7		elicopnf	⊢ ( 𝑀 ∈ ℝ → ( 𝑥 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑀 ≤ 𝑥 ) ) )
8	6 7	syl	⊢ ( 𝑀 ∈ ℤ → ( 𝑥 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑀 ≤ 𝑥 ) ) )
9	4 5 8	3imtr4d	⊢ ( 𝑀 ∈ ℤ → ( 𝑥 ∈ ( ℤ_≥ ‘ 𝑀 ) → 𝑥 ∈ ( 𝑀 [,) +∞ ) ) )
10	9	ssrdv	⊢ ( 𝑀 ∈ ℤ → ( ℤ_≥ ‘ 𝑀 ) ⊆ ( 𝑀 [,) +∞ ) )