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 ⊢ φ → M ∈ ℤ
liminflelimsupuz.2 ⊢ Z = ℤ ≥ M
liminflelimsupuz.3 ⊢ φ → F : Z ⟶ ℝ *
Assertion liminflelimsupuz ⊢ φ → lim inf ⁡ F ≤ lim sup ⁡ F

Proof

Step Hyp Ref Expression
1 liminflelimsupuz.1 ⊢ φ → M ∈ ℤ
2 liminflelimsupuz.2 ⊢ Z = ℤ ≥ M
3 liminflelimsupuz.3 ⊢ φ → F : Z ⟶ ℝ *
4 2 fvexi ⊢ Z ∈ V
5 4 a1i ⊢ φ → Z ∈ V
6 3 5 fexd ⊢ φ → F ∈ V
7 1 2 uzubico2 ⊢ φ → ∀ k ∈ ℝ ∃ j ∈ k +∞ j ∈ Z
8 3 ffnd ⊢ φ → F Fn Z
9 8 adantr ⊢ φ ∧ j ∈ Z → F Fn Z
10 simpr ⊢ φ ∧ j ∈ Z → j ∈ Z
11 id ⊢ j ∈ Z → j ∈ Z
12 2 11 uzxrd ⊢ j ∈ Z → j ∈ ℝ *
13 pnfxr ⊢ +∞ ∈ ℝ *
14 13 a1i ⊢ j ∈ Z → +∞ ∈ ℝ *
15 12 xrleidd ⊢ j ∈ Z → j ≤ j
16 2 11 uzred ⊢ j ∈ Z → j ∈ ℝ
17 ltpnf ⊢ j ∈ ℝ → j < +∞
18 16 17 syl ⊢ j ∈ Z → j < +∞
19 12 14 12 15 18 elicod ⊢ j ∈ Z → j ∈ j +∞
20 19 adantl ⊢ φ ∧ j ∈ Z → j ∈ j +∞
21 9 10 20 fnfvimad ⊢ φ ∧ j ∈ Z → F ⁡ j ∈ F j +∞
22 3 ffvelcdmda ⊢ φ ∧ j ∈ Z → F ⁡ j ∈ ℝ *
23 21 22 elind ⊢ φ ∧ j ∈ Z → F ⁡ j ∈ F j +∞ ∩ ℝ *
24 23 ne0d ⊢ φ ∧ j ∈ Z → F j +∞ ∩ ℝ * ≠ ∅
25 24 ex ⊢ φ → j ∈ Z → F j +∞ ∩ ℝ * ≠ ∅
26 25 ad2antrr ⊢ φ ∧ k ∈ ℝ ∧ j ∈ k +∞ → j ∈ Z → F j +∞ ∩ ℝ * ≠ ∅
27 26 reximdva ⊢ φ ∧ k ∈ ℝ → ∃ j ∈ k +∞ j ∈ Z → ∃ j ∈ k +∞ F j +∞ ∩ ℝ * ≠ ∅
28 27 ralimdva ⊢ φ → ∀ k ∈ ℝ ∃ j ∈ k +∞ j ∈ Z → ∀ k ∈ ℝ ∃ j ∈ k +∞ F j +∞ ∩ ℝ * ≠ ∅
29 7 28 mpd ⊢ φ → ∀ k ∈ ℝ ∃ j ∈ k +∞ F j +∞ ∩ ℝ * ≠ ∅
30 6 29 liminflelimsup ⊢ φ → lim inf ⁡ F ≤ lim sup ⁡ F