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	|- ( ph -> M e. ZZ )
	uzinico.2	|- Z = ( ZZ>= ` M )
Assertion	uzinico	|- ( ph -> Z = ( ZZ i^i ( M [,) +oo ) ) )

Proof

Step	Hyp	Ref	Expression
1		uzinico.1	|- ( ph -> M e. ZZ )
2		uzinico.2	|- Z = ( ZZ>= ` M )
3	2	eluzelz2	|- ( k e. Z -> k e. ZZ )
4	3	adantl	|- ( ( ph /\ k e. Z ) -> k e. ZZ )
5	1	zred	|- ( ph -> M e. RR )
6	5	rexrd	|- ( ph -> M e. RR* )
7	6	adantr	|- ( ( ph /\ k e. Z ) -> M e. RR* )
8		pnfxr	|- +oo e. RR*
9	8	a1i	|- ( ( ph /\ k e. Z ) -> +oo e. RR* )
10		zssre	|- ZZ C_ RR
11		ressxr	|- RR C_ RR*
12	10 11	sstri	|- ZZ C_ RR*
13	12 3	sseldi	|- ( k e. Z -> k e. RR* )
14	13	adantl	|- ( ( ph /\ k e. Z ) -> k e. RR* )
15	2	eleq2i	|- ( k e. Z <-> k e. ( ZZ>= ` M ) )
16	15	biimpi	|- ( k e. Z -> k e. ( ZZ>= ` M ) )
17		eluzle	|- ( k e. ( ZZ>= ` M ) -> M <_ k )
18	16 17	syl	|- ( k e. Z -> M <_ k )
19	18	adantl	|- ( ( ph /\ k e. Z ) -> M <_ k )
20	10 3	sseldi	|- ( k e. Z -> k e. RR )
21	20	ltpnfd	|- ( k e. Z -> k < +oo )
22	21	adantl	|- ( ( ph /\ k e. Z ) -> k < +oo )
23	7 9 14 19 22	elicod	|- ( ( ph /\ k e. Z ) -> k e. ( M [,) +oo ) )
24	4 23	elind	|- ( ( ph /\ k e. Z ) -> k e. ( ZZ i^i ( M [,) +oo ) ) )
25	24	ex	|- ( ph -> ( k e. Z -> k e. ( ZZ i^i ( M [,) +oo ) ) ) )
26	1	adantr	|- ( ( ph /\ k e. ( ZZ i^i ( M [,) +oo ) ) ) -> M e. ZZ )
27		elinel1	|- ( k e. ( ZZ i^i ( M [,) +oo ) ) -> k e. ZZ )
28	27	adantl	|- ( ( ph /\ k e. ( ZZ i^i ( M [,) +oo ) ) ) -> k e. ZZ )
29		elinel2	|- ( k e. ( ZZ i^i ( M [,) +oo ) ) -> k e. ( M [,) +oo ) )
30	29	adantl	|- ( ( ph /\ k e. ( ZZ i^i ( M [,) +oo ) ) ) -> k e. ( M [,) +oo ) )
31	6	adantr	|- ( ( ph /\ k e. ( M [,) +oo ) ) -> M e. RR* )
32	8	a1i	|- ( ( ph /\ k e. ( M [,) +oo ) ) -> +oo e. RR* )
33		simpr	|- ( ( ph /\ k e. ( M [,) +oo ) ) -> k e. ( M [,) +oo ) )
34	31 32 33	icogelbd	|- ( ( ph /\ k e. ( M [,) +oo ) ) -> M <_ k )
35	30 34	syldan	|- ( ( ph /\ k e. ( ZZ i^i ( M [,) +oo ) ) ) -> M <_ k )
36	2 26 28 35	eluzd	|- ( ( ph /\ k e. ( ZZ i^i ( M [,) +oo ) ) ) -> k e. Z )
37	36	ex	|- ( ph -> ( k e. ( ZZ i^i ( M [,) +oo ) ) -> k e. Z ) )
38	25 37	impbid	|- ( ph -> ( k e. Z <-> k e. ( ZZ i^i ( M [,) +oo ) ) ) )
39	38	alrimiv	|- ( ph -> A. k ( k e. Z <-> k e. ( ZZ i^i ( M [,) +oo ) ) ) )
40		dfcleq	|- ( Z = ( ZZ i^i ( M [,) +oo ) ) <-> A. k ( k e. Z <-> k e. ( ZZ i^i ( M [,) +oo ) ) ) )
41	39 40	sylibr	|- ( ph -> Z = ( ZZ i^i ( M [,) +oo ) ) )