Theorem uzinico

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

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

Proof

Step	Hyp	Ref	Expression
1		uzinico.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		uzinico.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3	2	eluzelz2	$$⊢k\in Z\to k\in \mathbb{Z}$$
4	3	adantl	$$⊢\left(\phi \wedge k\in Z\right)\to k\in \mathbb{Z}$$
5	1	zred	$$⊢\phi \to M\in ℝ$$
6	5	rexrd	$$⊢\phi \to M\in {ℝ}^{*}$$
7	6	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to M\in {ℝ}^{*}$$
8		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
9	8	a1i	$$⊢\left(\phi \wedge k\in Z\right)\to \mathrm{+\infty }\in {ℝ}^{*}$$
10		zssre	$$⊢\mathbb{Z}\subseteq ℝ$$
11		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
12	10 11	sstri	$$⊢\mathbb{Z}\subseteq {ℝ}^{*}$$
13	12 3	sseldi	$$⊢k\in Z\to k\in {ℝ}^{*}$$
14	13	adantl	$$⊢\left(\phi \wedge k\in Z\right)\to k\in {ℝ}^{*}$$
15	2	eleq2i	$$⊢k\in Z\leftrightarrow k\in {\mathbb{Z}}_{\ge M}$$
16	15	biimpi	$$⊢k\in Z\to k\in {\mathbb{Z}}_{\ge M}$$
17		eluzle	$$⊢k\in {\mathbb{Z}}_{\ge M}\to M\le k$$
18	16 17	syl	$$⊢k\in Z\to M\le k$$
19	18	adantl	$$⊢\left(\phi \wedge k\in Z\right)\to M\le k$$
20	10 3	sseldi	$$⊢k\in Z\to k\in ℝ$$
21	20	ltpnfd	$$⊢k\in Z\to k<\mathrm{+\infty }$$
22	21	adantl	$$⊢\left(\phi \wedge k\in Z\right)\to k<\mathrm{+\infty }$$
23	7 9 14 19 22	elicod	$$⊢\left(\phi \wedge k\in Z\right)\to k\in \left[M,\mathrm{+\infty }\right)$$
24	4 23	elind	$$⊢\left(\phi \wedge k\in Z\right)\to k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)$$
25	24	ex	$$⊢\phi \to \left(k\in Z\to k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\right)$$
26	1	adantr	$$⊢\left(\phi \wedge k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\right)\to M\in \mathbb{Z}$$
27		elinel1	$$⊢k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\to k\in \mathbb{Z}$$
28	27	adantl	$$⊢\left(\phi \wedge k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\right)\to k\in \mathbb{Z}$$
29		elinel2	$$⊢k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\to k\in \left[M,\mathrm{+\infty }\right)$$
30	29	adantl	$$⊢\left(\phi \wedge k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\right)\to k\in \left[M,\mathrm{+\infty }\right)$$
31	6	adantr	$$⊢\left(\phi \wedge k\in \left[M,\mathrm{+\infty }\right)\right)\to M\in {ℝ}^{*}$$
32	8	a1i	$$⊢\left(\phi \wedge k\in \left[M,\mathrm{+\infty }\right)\right)\to \mathrm{+\infty }\in {ℝ}^{*}$$
33		simpr	$$⊢\left(\phi \wedge k\in \left[M,\mathrm{+\infty }\right)\right)\to k\in \left[M,\mathrm{+\infty }\right)$$
34	31 32 33	icogelbd	$$⊢\left(\phi \wedge k\in \left[M,\mathrm{+\infty }\right)\right)\to M\le k$$
35	30 34	syldan	$$⊢\left(\phi \wedge k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\right)\to M\le k$$
36	2 26 28 35	eluzd	$$⊢\left(\phi \wedge k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\right)\to k\in Z$$
37	36	ex	$$⊢\phi \to \left(k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\to k\in Z\right)$$
38	25 37	impbid	$$⊢\phi \to \left(k\in Z\leftrightarrow k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\right)$$
39	38	alrimiv	$$⊢\phi \to \forall k\left(k\in Z\leftrightarrow k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\right)$$
40		dfcleq	$$⊢Z=\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\leftrightarrow \forall k\left(k\in Z\leftrightarrow k\in \left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)\right)$$
41	39 40	sylibr	$$⊢\phi \to Z=\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)$$