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	⊢ ( 𝜑 → 𝑍 = ( ℤ ∩ ( 𝑀 [,) +∞ ) ) )