This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem liminfpnfuz

Description: The inferior limit of a function is +oo if and only if every real number is the lower bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses liminfpnfuz.1 ⊢ Ⅎ 𝑗 𝐹
liminfpnfuz.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
liminfpnfuz.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
liminfpnfuz.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion liminfpnfuz ( 𝜑 → ( ( lim inf ‘ 𝐹 ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )

Proof

Step Hyp Ref Expression
1 liminfpnfuz.1 ⊢ Ⅎ 𝑗 𝐹
2 liminfpnfuz.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 liminfpnfuz.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 liminfpnfuz.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
5 nfv ⊢ Ⅎ 𝑙 𝜑
6 nfcv ⊢ Ⅎ 𝑙 𝐹
7 5 6 2 3 4 liminfvaluz3 ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑙 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑙 ) ) ) )
8 nfcv ⊢ Ⅎ 𝑗 𝑙
9 1 8 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
10 9 nfxneg ⊢ Ⅎ 𝑗 -𝑒 ( 𝐹 ‘ 𝑙 )
11 nfcv ⊢ Ⅎ 𝑙 -𝑒 ( 𝐹 ‘ 𝑗 )
12 fveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
13 12 xnegeqd ⊢ ( 𝑙 = 𝑗 → -𝑒 ( 𝐹 ‘ 𝑙 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
14 10 11 13 cbvmpt ⊢ ( 𝑙 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑙 ) ) = ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) )
15 14 fveq2i ⊢ ( lim sup ‘ ( 𝑙 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑙 ) ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) )
16 15 xnegeqi ⊢ -𝑒 ( lim sup ‘ ( 𝑙 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑙 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) )
17 7 16 eqtrdi ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) )
18 17 eqeq1d ⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) = +∞ ↔ -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = +∞ ) )
19 xnegmnf ⊢ -𝑒 -∞ = +∞
20 19 eqcomi ⊢ +∞ = -𝑒 -∞
21 20 a1i ⊢ ( 𝜑 → +∞ = -𝑒 -∞ )
22 21 eqeq2d ⊢ ( 𝜑 → ( -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = +∞ ↔ -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 -∞ ) )
23 3 fvexi ⊢ 𝑍 ∈ V
24 23 mptex ⊢ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ∈ V
25 24 a1i ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ∈ V )
26 25 limsupcld ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* )
27 mnfxr ⊢ -∞ ∈ ℝ*
28 xneg11 ⊢ ( ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 -∞ ↔ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -∞ ) )
29 26 27 28 sylancl ⊢ ( 𝜑 → ( -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 -∞ ↔ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -∞ ) )
30 22 29 bitrd ⊢ ( 𝜑 → ( -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = +∞ ↔ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -∞ ) )
31 3 uztrn2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 )
32 xnegex ⊢ -𝑒 ( 𝐹 ‘ 𝑗 ) ∈ V
33 fvmpt4 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ -𝑒 ( 𝐹 ‘ 𝑗 ) ∈ V ) → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
34 31 32 33 sylancl ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
35 34 breq1d ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
36 35 ralbidva ⊢ ( 𝑘 ∈ 𝑍 → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
37 36 rexbiia ⊢ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
38 37 ralbii ⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
39 38 a1i ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
40 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) )
41 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑙 ) ∈ ℝ* )
42 41 xnegcld ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑍 ) → -𝑒 ( 𝐹 ‘ 𝑙 ) ∈ ℝ* )
43 14 eqcomi ⊢ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) = ( 𝑙 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑙 ) )
44 42 43 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) : 𝑍 ⟶ ℝ* )
45 40 2 3 44 limsupmnfuz ⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ) )
46 1 3 4 xlimpnfxnegmnf ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
47 39 45 46 3bitr4d ⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
48 18 30 47 3bitrd ⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )