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 ffvelrnda ( ( 𝜑𝑙𝑍 ) → ( 𝐹𝑙 ) ∈ ℝ* )
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 ‘ 𝐹 ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ) )