Metamath Proof Explorer

Theorem liminflbuz2

Description: A sequence with values in the extended reals, and with liminf that is not -oo , is eventually greater than -oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses liminflbuz2.1 ⊢ Ⅎ 𝑗 𝜑
liminflbuz2.2 ⊢ Ⅎ 𝑗 𝐹
liminflbuz2.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
liminflbuz2.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
liminflbuz2.5 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
liminflbuz2.6 ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≠ -∞ )
Assertion liminflbuz2 ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -∞ < ( 𝐹 ‘ 𝑗 ) )

Proof

Step Hyp Ref Expression
1 liminflbuz2.1 ⊢ Ⅎ 𝑗 𝜑
2 liminflbuz2.2 ⊢ Ⅎ 𝑗 𝐹
3 liminflbuz2.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 liminflbuz2.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 liminflbuz2.5 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
6 liminflbuz2.6 ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≠ -∞ )
7 nfv ⊢ Ⅎ 𝑗 𝑘 ∈ 𝑍
8 1 7 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑘 ∈ 𝑍 )
9 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝜑 )
10 4 uztrn2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 )
11 10 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 )
12 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
13 12 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
14 mnfxr ⊢ -∞ ∈ ℝ*
15 14 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ -∞ < ( 𝐹 ‘ 𝑗 ) ) → -∞ ∈ ℝ* )
16 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ¬ -∞ < ( 𝐹 ‘ 𝑗 ) )
17 13 15 16 xrnltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ -∞ )
18 xlemnf ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ℝ* → ( ( 𝐹 ‘ 𝑗 ) ≤ -∞ ↔ ( 𝐹 ‘ 𝑗 ) = -∞ ) )
19 13 18 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑗 ) ≤ -∞ ↔ ( 𝐹 ‘ 𝑗 ) = -∞ ) )
20 17 19 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) = -∞ )
21 xnegeq ⊢ ( ( 𝐹 ‘ 𝑗 ) = -∞ → -𝑒 ( 𝐹 ‘ 𝑗 ) = -𝑒 -∞ )
22 xnegmnf ⊢ -𝑒 -∞ = +∞
23 21 22 eqtrdi ⊢ ( ( 𝐹 ‘ 𝑗 ) = -∞ → -𝑒 ( 𝐹 ‘ 𝑗 ) = +∞ )
24 20 23 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ -∞ < ( 𝐹 ‘ 𝑗 ) ) → -𝑒 ( 𝐹 ‘ 𝑗 ) = +∞ )
25 24 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ ) ∧ ¬ -∞ < ( 𝐹 ‘ 𝑗 ) ) → -𝑒 ( 𝐹 ‘ 𝑗 ) = +∞ )
26 neneq ⊢ ( -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ → ¬ -𝑒 ( 𝐹 ‘ 𝑗 ) = +∞ )
27 26 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ ) ∧ ¬ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ¬ -𝑒 ( 𝐹 ‘ 𝑗 ) = +∞ )
28 25 27 condan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ ) → -∞ < ( 𝐹 ‘ 𝑗 ) )
29 28 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ → -∞ < ( 𝐹 ‘ 𝑗 ) ) )
30 9 11 29 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ → -∞ < ( 𝐹 ‘ 𝑗 ) ) )
31 8 30 ralimdaa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -∞ < ( 𝐹 ‘ 𝑗 ) ) )
32 31 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -∞ < ( 𝐹 ‘ 𝑗 ) )
33 12 xnegcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → -𝑒 ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ ) → -𝑒 ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
35 pnfxr ⊢ +∞ ∈ ℝ*
36 35 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ ) → +∞ ∈ ℝ* )
37 eqidd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) = ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) )
38 37 33 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
39 38 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ ) → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ ) → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ )
41 39 40 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ ) → -𝑒 ( 𝐹 ‘ 𝑗 ) < +∞ )
42 34 36 41 xrltned ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ ) → -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ )
43 42 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ → -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ ) )
44 9 11 43 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ → -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ ) )
45 8 44 ralimdaa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ ) )
46 45 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ )
47 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) )
48 1 33 fmptd2f ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) : 𝑍 ⟶ ℝ* )
49 4 fvexi ⊢ 𝑍 ∈ V
50 49 a1i ⊢ ( 𝜑 → 𝑍 ∈ V )
51 5 50 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
52 51 liminfcld ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ* )
53 52 xnegnegd ⊢ ( 𝜑 → -𝑒 -𝑒 ( lim inf ‘ 𝐹 ) = ( lim inf ‘ 𝐹 ) )
54 1 2 3 4 5 liminfvaluz3 ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) )
55 53 54 eqtr2d ⊢ ( 𝜑 → -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 -𝑒 ( lim inf ‘ 𝐹 ) )
56 50 mptexd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ∈ V )
57 56 limsupcld ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* )
58 52 xnegcld ⊢ ( 𝜑 → -𝑒 ( lim inf ‘ 𝐹 ) ∈ ℝ* )
59 xneg11 ⊢ ( ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* ∧ -𝑒 ( lim inf ‘ 𝐹 ) ∈ ℝ* ) → ( -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 -𝑒 ( lim inf ‘ 𝐹 ) ↔ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 ( lim inf ‘ 𝐹 ) ) )
60 57 58 59 syl2anc ⊢ ( 𝜑 → ( -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 -𝑒 ( lim inf ‘ 𝐹 ) ↔ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 ( lim inf ‘ 𝐹 ) ) )
61 55 60 mpbid ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 ( lim inf ‘ 𝐹 ) )
62 nne ⊢ ( ¬ -𝑒 ( lim inf ‘ 𝐹 ) ≠ +∞ ↔ -𝑒 ( lim inf ‘ 𝐹 ) = +∞ )
63 53 eqcomd ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 -𝑒 ( lim inf ‘ 𝐹 ) )
64 63 adantr ⊢ ( ( 𝜑 ∧ -𝑒 ( lim inf ‘ 𝐹 ) = +∞ ) → ( lim inf ‘ 𝐹 ) = -𝑒 -𝑒 ( lim inf ‘ 𝐹 ) )
65 xnegeq ⊢ ( -𝑒 ( lim inf ‘ 𝐹 ) = +∞ → -𝑒 -𝑒 ( lim inf ‘ 𝐹 ) = -𝑒 +∞ )
66 65 adantl ⊢ ( ( 𝜑 ∧ -𝑒 ( lim inf ‘ 𝐹 ) = +∞ ) → -𝑒 -𝑒 ( lim inf ‘ 𝐹 ) = -𝑒 +∞ )
67 xnegpnf ⊢ -𝑒 +∞ = -∞
68 67 a1i ⊢ ( ( 𝜑 ∧ -𝑒 ( lim inf ‘ 𝐹 ) = +∞ ) → -𝑒 +∞ = -∞ )
69 64 66 68 3eqtrd ⊢ ( ( 𝜑 ∧ -𝑒 ( lim inf ‘ 𝐹 ) = +∞ ) → ( lim inf ‘ 𝐹 ) = -∞ )
70 62 69 sylan2b ⊢ ( ( 𝜑 ∧ ¬ -𝑒 ( lim inf ‘ 𝐹 ) ≠ +∞ ) → ( lim inf ‘ 𝐹 ) = -∞ )
71 6 neneqd ⊢ ( 𝜑 → ¬ ( lim inf ‘ 𝐹 ) = -∞ )
72 71 adantr ⊢ ( ( 𝜑 ∧ ¬ -𝑒 ( lim inf ‘ 𝐹 ) ≠ +∞ ) → ¬ ( lim inf ‘ 𝐹 ) = -∞ )
73 70 72 condan ⊢ ( 𝜑 → -𝑒 ( lim inf ‘ 𝐹 ) ≠ +∞ )
74 61 73 eqnetrd ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) ≠ +∞ )
75 1 47 3 4 48 74 limsupubuz2 ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) < +∞ )
76 46 75 reximddv3 ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≠ +∞ )
77 32 76 reximddv3 ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -∞ < ( 𝐹 ‘ 𝑗 ) )