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 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
uzinico.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion uzinico ( 𝜑 → 𝑍 = ( ℤ ∩ ( 𝑀 [,) +∞ ) ) )

Proof

Step Hyp Ref Expression
1 uzinico.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 uzinico.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 2 eluzelz2 ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
4 3 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℤ )
5 1 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
6 5 rexrd ⊢ ( 𝜑 → 𝑀 ∈ ℝ* )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑀 ∈ ℝ* )
8 pnfxr ⊢ +∞ ∈ ℝ*
9 8 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → +∞ ∈ ℝ* )
10 zssre ⊢ ℤ ⊆ ℝ
11 ressxr ⊢ ℝ ⊆ ℝ*
12 10 11 sstri ⊢ ℤ ⊆ ℝ*
13 12 3 sselid ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℝ* )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℝ* )
15 2 eleq2i ⊢ ( 𝑘 ∈ 𝑍 ↔ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
16 15 biimpi ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
17 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑘 )
18 16 17 syl ⊢ ( 𝑘 ∈ 𝑍 → 𝑀 ≤ 𝑘 )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑀 ≤ 𝑘 )
20 10 3 sselid ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℝ )
21 20 ltpnfd ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 < +∞ )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 < +∞ )
23 7 9 14 19 22 elicod ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ( 𝑀 [,) +∞ ) )
24 4 23 elind ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) )
25 24 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) )
26 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) → 𝑀 ∈ ℤ )
27 elinel1 ⊢ ( 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) → 𝑘 ∈ ℤ )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) → 𝑘 ∈ ℤ )
29 elinel2 ⊢ ( 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) → 𝑘 ∈ ( 𝑀 [,) +∞ ) )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) → 𝑘 ∈ ( 𝑀 [,) +∞ ) )
31 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ∈ ℝ* )
32 8 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 [,) +∞ ) ) → +∞ ∈ ℝ* )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 [,) +∞ ) ) → 𝑘 ∈ ( 𝑀 [,) +∞ ) )
34 31 32 33 icogelbd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ≤ 𝑘 )
35 30 34 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) → 𝑀 ≤ 𝑘 )
36 2 26 28 35 eluzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) → 𝑘 ∈ 𝑍 )
37 36 ex ⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) → 𝑘 ∈ 𝑍 ) )
38 25 37 impbid ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↔ 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) )
39 38 alrimiv ⊢ ( 𝜑 → ∀ 𝑘 ( 𝑘 ∈ 𝑍 ↔ 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) )
40 dfcleq ⊢ ( 𝑍 = ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ↔ ∀ 𝑘 ( 𝑘 ∈ 𝑍 ↔ 𝑘 ∈ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) )
41 39 40 sylibr ⊢ ( 𝜑 → 𝑍 = ( ℤ ∩ ( 𝑀 [,) +∞ ) ) )