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

Metamath Proof Explorer

Theorem uzinico3

Description: An upper interval of integers doesn't change when it's intersected with a left-closed, unbounded above interval, with the same lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	uzinico3.1	$⊢ φ \to M \in ℤ$
	uzinico3.2	$⊢ Z = ℤ_{\geq M}$
Assertion	uzinico3	$⊢ φ \to Z = Z \cap [M, +∞)$

Proof

Step	Hyp	Ref	Expression
1		uzinico3.1	$⊢ φ \to M \in ℤ$
2		uzinico3.2	$⊢ Z = ℤ_{\geq M}$
3	1	uzidd	$⊢ φ \to M \in ℤ_{\geq M}$
4	3	uzinico2	$⊢ φ \to ℤ_{\geq M} = ℤ_{\geq M} \cap [M, +∞)$
5	2	a1i	$⊢ φ \to Z = ℤ_{\geq M}$
6	5	ineq1d	$⊢ φ \to Z \cap [M, +∞) = ℤ_{\geq M} \cap [M, +∞)$
7	5 6	eqeq12d	$⊢ φ \to (Z = Z \cap [M, +∞) \leftrightarrow ℤ_{\geq M} = ℤ_{\geq M} \cap [M, +∞))$
8	4 7	mpbird	$⊢ φ \to Z = Z \cap [M, +∞)$