# Metamath Proof Explorer

## Theorem limsupresuz

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

Ref Expression
Hypotheses limsupresuz.m $⊢ φ → M ∈ ℤ$
limsupresuz.z $⊢ Z = ℤ ≥ M$
limsupresuz.f $⊢ φ → F ∈ V$
limsupresuz.d $⊢ φ → dom ⁡ F ↾ ℝ ⊆ ℤ$
Assertion limsupresuz $⊢ φ → lim sup ⁡ F ↾ Z = lim sup ⁡ F$

### Proof

Step Hyp Ref Expression
1 limsupresuz.m $⊢ φ → M ∈ ℤ$
2 limsupresuz.z $⊢ Z = ℤ ≥ M$
3 limsupresuz.f $⊢ φ → F ∈ V$
4 limsupresuz.d $⊢ φ → dom ⁡ F ↾ ℝ ⊆ ℤ$
5 rescom $⊢ F ↾ Z ↾ ℝ = F ↾ ℝ ↾ Z$
6 5 fveq2i $⊢ lim sup ⁡ F ↾ Z ↾ ℝ = lim sup ⁡ F ↾ ℝ ↾ Z$
7 6 a1i $⊢ φ → lim sup ⁡ F ↾ Z ↾ ℝ = lim sup ⁡ F ↾ ℝ ↾ Z$
8 relres $⊢ Rel ⁡ F ↾ ℝ$
9 8 a1i $⊢ φ → Rel ⁡ F ↾ ℝ$
10 relssres $⊢ Rel ⁡ F ↾ ℝ ∧ dom ⁡ F ↾ ℝ ⊆ ℤ → F ↾ ℝ ↾ ℤ = F ↾ ℝ$
11 9 4 10 syl2anc $⊢ φ → F ↾ ℝ ↾ ℤ = F ↾ ℝ$
12 11 eqcomd $⊢ φ → F ↾ ℝ = F ↾ ℝ ↾ ℤ$
13 12 reseq1d $⊢ φ → F ↾ ℝ ↾ M +∞ = F ↾ ℝ ↾ ℤ ↾ M +∞$
14 resres $⊢ F ↾ ℝ ↾ ℤ ↾ M +∞ = F ↾ ℝ ↾ ℤ ∩ M +∞$
15 14 a1i $⊢ φ → F ↾ ℝ ↾ ℤ ↾ M +∞ = F ↾ ℝ ↾ ℤ ∩ M +∞$
16 1 2 uzinico $⊢ φ → Z = ℤ ∩ M +∞$
17 16 eqcomd $⊢ φ → ℤ ∩ M +∞ = Z$
18 17 reseq2d $⊢ φ → F ↾ ℝ ↾ ℤ ∩ M +∞ = F ↾ ℝ ↾ Z$
19 13 15 18 3eqtrrd $⊢ φ → F ↾ ℝ ↾ Z = F ↾ ℝ ↾ M +∞$
20 19 fveq2d $⊢ φ → lim sup ⁡ F ↾ ℝ ↾ Z = lim sup ⁡ F ↾ ℝ ↾ M +∞$
21 1 zred $⊢ φ → M ∈ ℝ$
22 eqid $⊢ M +∞ = M +∞$
23 3 resexd $⊢ φ → F ↾ ℝ ∈ V$
24 21 22 23 limsupresico $⊢ φ → lim sup ⁡ F ↾ ℝ ↾ M +∞ = lim sup ⁡ F ↾ ℝ$
25 20 24 eqtrd $⊢ φ → lim sup ⁡ F ↾ ℝ ↾ Z = lim sup ⁡ F ↾ ℝ$
26 7 25 eqtrd $⊢ φ → lim sup ⁡ F ↾ Z ↾ ℝ = lim sup ⁡ F ↾ ℝ$
27 3 resexd $⊢ φ → F ↾ Z ∈ V$
28 27 limsupresre $⊢ φ → lim sup ⁡ F ↾ Z ↾ ℝ = lim sup ⁡ F ↾ Z$
29 3 limsupresre $⊢ φ → lim sup ⁡ F ↾ ℝ = lim sup ⁡ F$
30 26 28 29 3eqtr3d $⊢ φ → lim sup ⁡ F ↾ Z = lim sup ⁡ F$