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 φ M
uzinico.2 Z = M
Assertion uzinico φ Z = M +∞

Proof

Step Hyp Ref Expression
1 uzinico.1 φ M
2 uzinico.2 Z = M
3 2 eluzelz2 k Z k
4 3 adantl φ k Z k
5 1 zred φ M
6 5 rexrd φ M *
7 6 adantr φ k Z M *
8 pnfxr +∞ *
9 8 a1i φ k Z +∞ *
10 zssre
11 ressxr *
12 10 11 sstri *
13 12 3 sselid k Z k *
14 13 adantl φ k Z k *
15 2 eleq2i k Z k M
16 15 biimpi k Z k M
17 eluzle k M M k
18 16 17 syl k Z M k
19 18 adantl φ k Z M k
20 10 3 sselid k Z k
21 20 ltpnfd k Z k < +∞
22 21 adantl φ k Z k < +∞
23 7 9 14 19 22 elicod φ k Z k M +∞
24 4 23 elind φ k Z k M +∞
25 24 ex φ k Z k M +∞
26 1 adantr φ k M +∞ M
27 elinel1 k M +∞ k
28 27 adantl φ k M +∞ k
29 elinel2 k M +∞ k M +∞
30 29 adantl φ k M +∞ k M +∞
31 6 adantr φ k M +∞ M *
32 8 a1i φ k M +∞ +∞ *
33 simpr φ k M +∞ k M +∞
34 31 32 33 icogelbd φ k M +∞ M k
35 30 34 syldan φ k M +∞ M k
36 2 26 28 35 eluzd φ k M +∞ k Z
37 36 ex φ k M +∞ k Z
38 25 37 impbid φ k Z k M +∞
39 38 alrimiv φ k k Z k M +∞
40 dfcleq Z = M +∞ k k Z k M +∞
41 39 40 sylibr φ Z = M +∞