Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  liminflbuz2 Structured version   Visualization version   GIF version

Theorem liminflbuz2 42452
 Description: A sequence with values in the extended reals, and with liminf that is not -∞, is eventually greater than -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
Hypotheses
Ref Expression
liminflbuz2.1 𝑗𝜑
liminflbuz2.2 𝑗𝐹
liminflbuz2.3 (𝜑𝑀 ∈ ℤ)
liminflbuz2.4 𝑍 = (ℤ𝑀)
liminflbuz2.5 (𝜑𝐹:𝑍⟶ℝ*)
liminflbuz2.6 (𝜑 → (lim inf‘𝐹) ≠ -∞)
Assertion
Ref Expression
liminflbuz2 (𝜑 → ∃𝑘𝑍𝑗 ∈ (ℤ𝑘)-∞ < (𝐹𝑗))
Distinct variable groups:   𝑘,𝐹   𝑗,𝑀,𝑘   𝑗,𝑍,𝑘   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑗)   𝐹(𝑗)

Proof of Theorem liminflbuz2
StepHypRef Expression
1 liminflbuz2.1 . . . . 5 𝑗𝜑
2 nfv 1915 . . . . 5 𝑗 𝑘𝑍
31, 2nfan 1900 . . . 4 𝑗(𝜑𝑘𝑍)
4 simpll 766 . . . . 5 (((𝜑𝑘𝑍) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝜑)
5 liminflbuz2.4 . . . . . . 7 𝑍 = (ℤ𝑀)
65uztrn2 12250 . . . . . 6 ((𝑘𝑍𝑗 ∈ (ℤ𝑘)) → 𝑗𝑍)
76adantll 713 . . . . 5 (((𝜑𝑘𝑍) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑗𝑍)
8 liminflbuz2.5 . . . . . . . . . . . . 13 (𝜑𝐹:𝑍⟶ℝ*)
98ffvelrnda 6828 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → (𝐹𝑗) ∈ ℝ*)
109adantr 484 . . . . . . . . . . 11 (((𝜑𝑗𝑍) ∧ ¬ -∞ < (𝐹𝑗)) → (𝐹𝑗) ∈ ℝ*)
11 mnfxr 10687 . . . . . . . . . . . 12 -∞ ∈ ℝ*
1211a1i 11 . . . . . . . . . . 11 (((𝜑𝑗𝑍) ∧ ¬ -∞ < (𝐹𝑗)) → -∞ ∈ ℝ*)
13 simpr 488 . . . . . . . . . . 11 (((𝜑𝑗𝑍) ∧ ¬ -∞ < (𝐹𝑗)) → ¬ -∞ < (𝐹𝑗))
1410, 12, 13xrnltled 10698 . . . . . . . . . 10 (((𝜑𝑗𝑍) ∧ ¬ -∞ < (𝐹𝑗)) → (𝐹𝑗) ≤ -∞)
15 xlemnf 12548 . . . . . . . . . . 11 ((𝐹𝑗) ∈ ℝ* → ((𝐹𝑗) ≤ -∞ ↔ (𝐹𝑗) = -∞))
1610, 15syl 17 . . . . . . . . . 10 (((𝜑𝑗𝑍) ∧ ¬ -∞ < (𝐹𝑗)) → ((𝐹𝑗) ≤ -∞ ↔ (𝐹𝑗) = -∞))
1714, 16mpbid 235 . . . . . . . . 9 (((𝜑𝑗𝑍) ∧ ¬ -∞ < (𝐹𝑗)) → (𝐹𝑗) = -∞)
18 xnegeq 12588 . . . . . . . . . 10 ((𝐹𝑗) = -∞ → -𝑒(𝐹𝑗) = -𝑒-∞)
19 xnegmnf 12591 . . . . . . . . . 10 -𝑒-∞ = +∞
2018, 19eqtrdi 2849 . . . . . . . . 9 ((𝐹𝑗) = -∞ → -𝑒(𝐹𝑗) = +∞)
2117, 20syl 17 . . . . . . . 8 (((𝜑𝑗𝑍) ∧ ¬ -∞ < (𝐹𝑗)) → -𝑒(𝐹𝑗) = +∞)
2221adantlr 714 . . . . . . 7 ((((𝜑𝑗𝑍) ∧ -𝑒(𝐹𝑗) ≠ +∞) ∧ ¬ -∞ < (𝐹𝑗)) → -𝑒(𝐹𝑗) = +∞)
23 neneq 2993 . . . . . . . 8 (-𝑒(𝐹𝑗) ≠ +∞ → ¬ -𝑒(𝐹𝑗) = +∞)
2423ad2antlr 726 . . . . . . 7 ((((𝜑𝑗𝑍) ∧ -𝑒(𝐹𝑗) ≠ +∞) ∧ ¬ -∞ < (𝐹𝑗)) → ¬ -𝑒(𝐹𝑗) = +∞)
2522, 24condan 817 . . . . . 6 (((𝜑𝑗𝑍) ∧ -𝑒(𝐹𝑗) ≠ +∞) → -∞ < (𝐹𝑗))
2625ex 416 . . . . 5 ((𝜑𝑗𝑍) → (-𝑒(𝐹𝑗) ≠ +∞ → -∞ < (𝐹𝑗)))
274, 7, 26syl2anc 587 . . . 4 (((𝜑𝑘𝑍) ∧ 𝑗 ∈ (ℤ𝑘)) → (-𝑒(𝐹𝑗) ≠ +∞ → -∞ < (𝐹𝑗)))
283, 27ralimdaa 3181 . . 3 ((𝜑𝑘𝑍) → (∀𝑗 ∈ (ℤ𝑘)-𝑒(𝐹𝑗) ≠ +∞ → ∀𝑗 ∈ (ℤ𝑘)-∞ < (𝐹𝑗)))
2928imp 410 . 2 (((𝜑𝑘𝑍) ∧ ∀𝑗 ∈ (ℤ𝑘)-𝑒(𝐹𝑗) ≠ +∞) → ∀𝑗 ∈ (ℤ𝑘)-∞ < (𝐹𝑗))
309xnegcld 12681 . . . . . . . . 9 ((𝜑𝑗𝑍) → -𝑒(𝐹𝑗) ∈ ℝ*)
3130adantr 484 . . . . . . . 8 (((𝜑𝑗𝑍) ∧ ((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞) → -𝑒(𝐹𝑗) ∈ ℝ*)
32 pnfxr 10684 . . . . . . . . 9 +∞ ∈ ℝ*
3332a1i 11 . . . . . . . 8 (((𝜑𝑗𝑍) ∧ ((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞) → +∞ ∈ ℝ*)
34 eqidd 2799 . . . . . . . . . . 11 (𝜑 → (𝑗𝑍 ↦ -𝑒(𝐹𝑗)) = (𝑗𝑍 ↦ -𝑒(𝐹𝑗)))
3534, 30fvmpt2d 6758 . . . . . . . . . 10 ((𝜑𝑗𝑍) → ((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) = -𝑒(𝐹𝑗))
3635adantr 484 . . . . . . . . 9 (((𝜑𝑗𝑍) ∧ ((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞) → ((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) = -𝑒(𝐹𝑗))
37 simpr 488 . . . . . . . . 9 (((𝜑𝑗𝑍) ∧ ((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞) → ((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞)
3836, 37eqbrtrrd 5054 . . . . . . . 8 (((𝜑𝑗𝑍) ∧ ((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞) → -𝑒(𝐹𝑗) < +∞)
3931, 33, 38xrltned 41984 . . . . . . 7 (((𝜑𝑗𝑍) ∧ ((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞) → -𝑒(𝐹𝑗) ≠ +∞)
4039ex 416 . . . . . 6 ((𝜑𝑗𝑍) → (((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞ → -𝑒(𝐹𝑗) ≠ +∞))
414, 7, 40syl2anc 587 . . . . 5 (((𝜑𝑘𝑍) ∧ 𝑗 ∈ (ℤ𝑘)) → (((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞ → -𝑒(𝐹𝑗) ≠ +∞))
423, 41ralimdaa 3181 . . . 4 ((𝜑𝑘𝑍) → (∀𝑗 ∈ (ℤ𝑘)((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞ → ∀𝑗 ∈ (ℤ𝑘)-𝑒(𝐹𝑗) ≠ +∞))
4342imp 410 . . 3 (((𝜑𝑘𝑍) ∧ ∀𝑗 ∈ (ℤ𝑘)((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞) → ∀𝑗 ∈ (ℤ𝑘)-𝑒(𝐹𝑗) ≠ +∞)
44 nfmpt1 5128 . . . 4 𝑗(𝑗𝑍 ↦ -𝑒(𝐹𝑗))
45 liminflbuz2.3 . . . 4 (𝜑𝑀 ∈ ℤ)
461, 30fmptd2f 41866 . . . 4 (𝜑 → (𝑗𝑍 ↦ -𝑒(𝐹𝑗)):𝑍⟶ℝ*)
475fvexi 6659 . . . . . . . . . . 11 𝑍 ∈ V
4847a1i 11 . . . . . . . . . 10 (𝜑𝑍 ∈ V)
498, 48fexd 6967 . . . . . . . . 9 (𝜑𝐹 ∈ V)
5049liminfcld 42407 . . . . . . . 8 (𝜑 → (lim inf‘𝐹) ∈ ℝ*)
5150xnegnegd 42074 . . . . . . 7 (𝜑 → -𝑒-𝑒(lim inf‘𝐹) = (lim inf‘𝐹))
52 liminflbuz2.2 . . . . . . . 8 𝑗𝐹
531, 52, 45, 5, 8liminfvaluz3 42433 . . . . . . 7 (𝜑 → (lim inf‘𝐹) = -𝑒(lim sup‘(𝑗𝑍 ↦ -𝑒(𝐹𝑗))))
5451, 53eqtr2d 2834 . . . . . 6 (𝜑 → -𝑒(lim sup‘(𝑗𝑍 ↦ -𝑒(𝐹𝑗))) = -𝑒-𝑒(lim inf‘𝐹))
5548mptexd 6964 . . . . . . . 8 (𝜑 → (𝑗𝑍 ↦ -𝑒(𝐹𝑗)) ∈ V)
5655limsupcld 42327 . . . . . . 7 (𝜑 → (lim sup‘(𝑗𝑍 ↦ -𝑒(𝐹𝑗))) ∈ ℝ*)
5750xnegcld 12681 . . . . . . 7 (𝜑 → -𝑒(lim inf‘𝐹) ∈ ℝ*)
58 xneg11 12596 . . . . . . 7 (((lim sup‘(𝑗𝑍 ↦ -𝑒(𝐹𝑗))) ∈ ℝ* ∧ -𝑒(lim inf‘𝐹) ∈ ℝ*) → (-𝑒(lim sup‘(𝑗𝑍 ↦ -𝑒(𝐹𝑗))) = -𝑒-𝑒(lim inf‘𝐹) ↔ (lim sup‘(𝑗𝑍 ↦ -𝑒(𝐹𝑗))) = -𝑒(lim inf‘𝐹)))
5956, 57, 58syl2anc 587 . . . . . 6 (𝜑 → (-𝑒(lim sup‘(𝑗𝑍 ↦ -𝑒(𝐹𝑗))) = -𝑒-𝑒(lim inf‘𝐹) ↔ (lim sup‘(𝑗𝑍 ↦ -𝑒(𝐹𝑗))) = -𝑒(lim inf‘𝐹)))
6054, 59mpbid 235 . . . . 5 (𝜑 → (lim sup‘(𝑗𝑍 ↦ -𝑒(𝐹𝑗))) = -𝑒(lim inf‘𝐹))
61 nne 2991 . . . . . . 7 (¬ -𝑒(lim inf‘𝐹) ≠ +∞ ↔ -𝑒(lim inf‘𝐹) = +∞)
6251eqcomd 2804 . . . . . . . . 9 (𝜑 → (lim inf‘𝐹) = -𝑒-𝑒(lim inf‘𝐹))
6362adantr 484 . . . . . . . 8 ((𝜑 ∧ -𝑒(lim inf‘𝐹) = +∞) → (lim inf‘𝐹) = -𝑒-𝑒(lim inf‘𝐹))
64 xnegeq 12588 . . . . . . . . 9 (-𝑒(lim inf‘𝐹) = +∞ → -𝑒-𝑒(lim inf‘𝐹) = -𝑒+∞)
6564adantl 485 . . . . . . . 8 ((𝜑 ∧ -𝑒(lim inf‘𝐹) = +∞) → -𝑒-𝑒(lim inf‘𝐹) = -𝑒+∞)
66 xnegpnf 12590 . . . . . . . . 9 -𝑒+∞ = -∞
6766a1i 11 . . . . . . . 8 ((𝜑 ∧ -𝑒(lim inf‘𝐹) = +∞) → -𝑒+∞ = -∞)
6863, 65, 673eqtrd 2837 . . . . . . 7 ((𝜑 ∧ -𝑒(lim inf‘𝐹) = +∞) → (lim inf‘𝐹) = -∞)
6961, 68sylan2b 596 . . . . . 6 ((𝜑 ∧ ¬ -𝑒(lim inf‘𝐹) ≠ +∞) → (lim inf‘𝐹) = -∞)
70 liminflbuz2.6 . . . . . . . 8 (𝜑 → (lim inf‘𝐹) ≠ -∞)
7170neneqd 2992 . . . . . . 7 (𝜑 → ¬ (lim inf‘𝐹) = -∞)
7271adantr 484 . . . . . 6 ((𝜑 ∧ ¬ -𝑒(lim inf‘𝐹) ≠ +∞) → ¬ (lim inf‘𝐹) = -∞)
7369, 72condan 817 . . . . 5 (𝜑 → -𝑒(lim inf‘𝐹) ≠ +∞)
7460, 73eqnetrd 3054 . . . 4 (𝜑 → (lim sup‘(𝑗𝑍 ↦ -𝑒(𝐹𝑗))) ≠ +∞)
751, 44, 45, 5, 46, 74limsupubuz2 42450 . . 3 (𝜑 → ∃𝑘𝑍𝑗 ∈ (ℤ𝑘)((𝑗𝑍 ↦ -𝑒(𝐹𝑗))‘𝑗) < +∞)
7643, 75reximddv3 41783 . 2 (𝜑 → ∃𝑘𝑍𝑗 ∈ (ℤ𝑘)-𝑒(𝐹𝑗) ≠ +∞)
7729, 76reximddv3 41783 1 (𝜑 → ∃𝑘𝑍𝑗 ∈ (ℤ𝑘)-∞ < (𝐹𝑗))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  Ⅎwnf 1785   ∈ wcel 2111  Ⅎwnfc 2936   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   class class class wbr 5030   ↦ cmpt 5110  ⟶wf 6320  ‘cfv 6324  +∞cpnf 10661  -∞cmnf 10662  ℝ*cxr 10663   < clt 10664   ≤ cle 10665  ℤcz 11969  ℤ≥cuz 12231  -𝑒cxne 12492  lim supclsp 14819  lim infclsi 42388 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-sup 8890  df-inf 8891  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-n0 11886  df-z 11970  df-uz 12232  df-q 12337  df-xneg 12495  df-ico 12732  df-fl 13157  df-limsup 14820  df-liminf 42389 This theorem is referenced by:  liminflimsupxrre  42454
 Copyright terms: Public domain W3C validator