# Metamath Proof Explorer

## Theorem liminflelimsupuz

Description: The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminflelimsupuz.1 ( 𝜑𝑀 ∈ ℤ )
liminflelimsupuz.2 𝑍 = ( ℤ𝑀 )
liminflelimsupuz.3 ( 𝜑𝐹 : 𝑍 ⟶ ℝ* )
Assertion liminflelimsupuz ( 𝜑 → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )

### Proof

Step Hyp Ref Expression
1 liminflelimsupuz.1 ( 𝜑𝑀 ∈ ℤ )
2 liminflelimsupuz.2 𝑍 = ( ℤ𝑀 )
3 liminflelimsupuz.3 ( 𝜑𝐹 : 𝑍 ⟶ ℝ* )
4 2 fvexi 𝑍 ∈ V
5 4 a1i ( 𝜑𝑍 ∈ V )
6 3 5 fexd ( 𝜑𝐹 ∈ V )
7 1 2 uzubico2 ( 𝜑 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) 𝑗𝑍 )
8 3 ffnd ( 𝜑𝐹 Fn 𝑍 )
9 8 adantr ( ( 𝜑𝑗𝑍 ) → 𝐹 Fn 𝑍 )
10 simpr ( ( 𝜑𝑗𝑍 ) → 𝑗𝑍 )
11 id ( 𝑗𝑍𝑗𝑍 )
12 2 11 uzxrd ( 𝑗𝑍𝑗 ∈ ℝ* )
13 pnfxr +∞ ∈ ℝ*
14 13 a1i ( 𝑗𝑍 → +∞ ∈ ℝ* )
15 12 xrleidd ( 𝑗𝑍𝑗𝑗 )
16 2 11 uzred ( 𝑗𝑍𝑗 ∈ ℝ )
17 ltpnf ( 𝑗 ∈ ℝ → 𝑗 < +∞ )
18 16 17 syl ( 𝑗𝑍𝑗 < +∞ )
19 12 14 12 15 18 elicod ( 𝑗𝑍𝑗 ∈ ( 𝑗 [,) +∞ ) )
20 19 adantl ( ( 𝜑𝑗𝑍 ) → 𝑗 ∈ ( 𝑗 [,) +∞ ) )
21 9 10 20 fnfvimad ( ( 𝜑𝑗𝑍 ) → ( 𝐹𝑗 ) ∈ ( 𝐹 “ ( 𝑗 [,) +∞ ) ) )
22 3 ffvelrnda ( ( 𝜑𝑗𝑍 ) → ( 𝐹𝑗 ) ∈ ℝ* )
23 21 22 elind ( ( 𝜑𝑗𝑍 ) → ( 𝐹𝑗 ) ∈ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) )
24 23 ne0d ( ( 𝜑𝑗𝑍 ) → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
25 24 ex ( 𝜑 → ( 𝑗𝑍 → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) )
26 25 ad2antrr ( ( ( 𝜑𝑘 ∈ ℝ ) ∧ 𝑗 ∈ ( 𝑘 [,) +∞ ) ) → ( 𝑗𝑍 → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) )
27 26 reximdva ( ( 𝜑𝑘 ∈ ℝ ) → ( ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) 𝑗𝑍 → ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) )
28 27 ralimdva ( 𝜑 → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) 𝑗𝑍 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) )
29 7 28 mpd ( 𝜑 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
30 6 29 liminflelimsup ( 𝜑 → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )