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

Metamath Proof Explorer

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 sselid 
 |-  ( 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 sselid 
 |-  ( 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 ) ) )