Metamath Proof Explorer

Theorem liminfresuz

Description: If the real part of the domain of a function is a subset of the integers, the inferior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfresuz.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
liminfresuz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
liminfresuz.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
liminfresuz.d ⊢ ( 𝜑 → dom ( 𝐹 ↾ ℝ ) ⊆ ℤ )
Assertion liminfresuz ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ 𝑍 ) ) = ( lim inf ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 liminfresuz.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 liminfresuz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 liminfresuz.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
4 liminfresuz.d ⊢ ( 𝜑 → dom ( 𝐹 ↾ ℝ ) ⊆ ℤ )
5 rescom ⊢ ( ( 𝐹 ↾ 𝑍 ) ↾ ℝ ) = ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 )
6 5 fveq2i ⊢ ( lim inf ‘ ( ( 𝐹 ↾ 𝑍 ) ↾ ℝ ) ) = ( lim inf ‘ ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) )
7 6 a1i ⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝐹 ↾ 𝑍 ) ↾ ℝ ) ) = ( lim inf ‘ ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) ) )
8 relres ⊢ Rel ( 𝐹 ↾ ℝ )
9 8 a1i ⊢ ( 𝜑 → Rel ( 𝐹 ↾ ℝ ) )
10 relssres ⊢ ( ( Rel ( 𝐹 ↾ ℝ ) ∧ dom ( 𝐹 ↾ ℝ ) ⊆ ℤ ) → ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) = ( 𝐹 ↾ ℝ ) )
11 9 4 10 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) = ( 𝐹 ↾ ℝ ) )
12 11 eqcomd ⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) = ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) )
13 12 reseq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ↾ ( 𝑀 [,) +∞ ) ) = ( ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) ↾ ( 𝑀 [,) +∞ ) ) )
14 resres ⊢ ( ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) ↾ ( 𝑀 [,) +∞ ) ) = ( ( 𝐹 ↾ ℝ ) ↾ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) )
15 14 a1i ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) ↾ ( 𝑀 [,) +∞ ) ) = ( ( 𝐹 ↾ ℝ ) ↾ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) )
16 1 2 uzinico ⊢ ( 𝜑 → 𝑍 = ( ℤ ∩ ( 𝑀 [,) +∞ ) ) )
17 16 eqcomd ⊢ ( 𝜑 → ( ℤ ∩ ( 𝑀 [,) +∞ ) ) = 𝑍 )
18 17 reseq2d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ↾ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) = ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) )
19 13 15 18 3eqtrrd ⊢ ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) = ( ( 𝐹 ↾ ℝ ) ↾ ( 𝑀 [,) +∞ ) ) )
20 19 fveq2d ⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) ) = ( lim inf ‘ ( ( 𝐹 ↾ ℝ ) ↾ ( 𝑀 [,) +∞ ) ) ) )
21 1 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
22 eqid ⊢ ( 𝑀 [,) +∞ ) = ( 𝑀 [,) +∞ )
23 3 resexd ⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) ∈ V )
24 21 22 23 liminfresico ⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝐹 ↾ ℝ ) ↾ ( 𝑀 [,) +∞ ) ) ) = ( lim inf ‘ ( 𝐹 ↾ ℝ ) ) )
25 20 24 eqtrd ⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) ) = ( lim inf ‘ ( 𝐹 ↾ ℝ ) ) )
26 7 25 eqtrd ⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝐹 ↾ 𝑍 ) ↾ ℝ ) ) = ( lim inf ‘ ( 𝐹 ↾ ℝ ) ) )
27 3 resexd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑍 ) ∈ V )
28 27 liminfresre ⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝐹 ↾ 𝑍 ) ↾ ℝ ) ) = ( lim inf ‘ ( 𝐹 ↾ 𝑍 ) ) )
29 3 liminfresre ⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ ℝ ) ) = ( lim inf ‘ 𝐹 ) )
30 26 28 29 3eqtr3d ⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ 𝑍 ) ) = ( lim inf ‘ 𝐹 ) )