Theorem uzinico2

Description: An upper interval of integers is the intersection of a larger upper interval of integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypothesis	uzinico2.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
Assertion	uzinico2	$$⊢\phi \to {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge M}\cap \left[N,\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		uzinico2.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
2		inass	$$⊢\left({\mathbb{Z}}_{\ge M}\cap \mathbb{Z}\right)\cap \left[N,\mathrm{+\infty }\right)={\mathbb{Z}}_{\ge M}\cap \left(\mathbb{Z}\cap \left[N,\mathrm{+\infty }\right)\right)$$
3	2	a1i	$$⊢\phi \to \left({\mathbb{Z}}_{\ge M}\cap \mathbb{Z}\right)\cap \left[N,\mathrm{+\infty }\right)={\mathbb{Z}}_{\ge M}\cap \left(\mathbb{Z}\cap \left[N,\mathrm{+\infty }\right)\right)$$
4		incom	$$⊢{\mathbb{Z}}_{\ge M}\cap \left(\mathbb{Z}\cap \left[N,\mathrm{+\infty }\right)\right)=\left(\mathbb{Z}\cap \left[N,\mathrm{+\infty }\right)\right)\cap {\mathbb{Z}}_{\ge M}$$
5	4	a1i	$$⊢\phi \to {\mathbb{Z}}_{\ge M}\cap \left(\mathbb{Z}\cap \left[N,\mathrm{+\infty }\right)\right)=\left(\mathbb{Z}\cap \left[N,\mathrm{+\infty }\right)\right)\cap {\mathbb{Z}}_{\ge M}$$
6		uzssz	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}$$
7	6	a1i	$$⊢\phi \to {\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}$$
8	7 1	sseldd	$$⊢\phi \to N\in \mathbb{Z}$$
9		eqid	$$⊢{\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge N}$$
10	8 9	uzinico	$$⊢\phi \to {\mathbb{Z}}_{\ge N}=\mathbb{Z}\cap \left[N,\mathrm{+\infty }\right)$$
11	10	eqcomd	$$⊢\phi \to \mathbb{Z}\cap \left[N,\mathrm{+\infty }\right)={\mathbb{Z}}_{\ge N}$$
12	11	ineq1d	$$⊢\phi \to \left(\mathbb{Z}\cap \left[N,\mathrm{+\infty }\right)\right)\cap {\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge N}\cap {\mathbb{Z}}_{\ge M}$$
13	1	uzssd	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}$$
14		df-ss	$$⊢{\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}\leftrightarrow {\mathbb{Z}}_{\ge N}\cap {\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge N}$$
15	13 14	sylib	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\cap {\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge N}$$
16	5 12 15	3eqtrd	$$⊢\phi \to {\mathbb{Z}}_{\ge M}\cap \left(\mathbb{Z}\cap \left[N,\mathrm{+\infty }\right)\right)={\mathbb{Z}}_{\ge N}$$
17		uzssz	$$⊢{\mathbb{Z}}_{\ge N}\subseteq \mathbb{Z}$$
18		df-ss	$$⊢{\mathbb{Z}}_{\ge N}\subseteq \mathbb{Z}\leftrightarrow {\mathbb{Z}}_{\ge N}\cap \mathbb{Z}={\mathbb{Z}}_{\ge N}$$
19	17 18	mpbi	$$⊢{\mathbb{Z}}_{\ge N}\cap \mathbb{Z}={\mathbb{Z}}_{\ge N}$$
20	19	a1i	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\cap \mathbb{Z}={\mathbb{Z}}_{\ge N}$$
21	20	eqcomd	$$⊢\phi \to {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge N}\cap \mathbb{Z}$$
22	3 16 21	3eqtrrd	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\cap \mathbb{Z}=\left({\mathbb{Z}}_{\ge M}\cap \mathbb{Z}\right)\cap \left[N,\mathrm{+\infty }\right)$$
23		df-ss	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}\leftrightarrow {\mathbb{Z}}_{\ge M}\cap \mathbb{Z}={\mathbb{Z}}_{\ge M}$$
24	6 23	mpbi	$$⊢{\mathbb{Z}}_{\ge M}\cap \mathbb{Z}={\mathbb{Z}}_{\ge M}$$
25	24	ineq1i	$$⊢\left({\mathbb{Z}}_{\ge M}\cap \mathbb{Z}\right)\cap \left[N,\mathrm{+\infty }\right)={\mathbb{Z}}_{\ge M}\cap \left[N,\mathrm{+\infty }\right)$$
26	25	a1i	$$⊢\phi \to \left({\mathbb{Z}}_{\ge M}\cap \mathbb{Z}\right)\cap \left[N,\mathrm{+\infty }\right)={\mathbb{Z}}_{\ge M}\cap \left[N,\mathrm{+\infty }\right)$$
27	22 20 26	3eqtr3d	$$⊢\phi \to {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge M}\cap \left[N,\mathrm{+\infty }\right)$$