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

Metamath Proof Explorer

Theorem liminflimsupxrre

Description: A sequence with values in the extended reals, and with real liminf and limsup, is eventually real. (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses liminflimsupxrre.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
liminflimsupxrre.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
liminflimsupxrre.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
liminflimsupxrre.4 ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
liminflimsupxrre.5 ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≠ -∞ )
Assertion liminflimsupxrre ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 liminflimsupxrre.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 liminflimsupxrre.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 liminflimsupxrre.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 liminflimsupxrre.4 ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
5 liminflimsupxrre.5 ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≠ -∞ )
6 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝜑 )
7 2 uztrn2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 )
8 7 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
10 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑍 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → dom 𝐹 = 𝑍 )
12 9 11 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ dom 𝐹 )
13 12 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑗 ) < +∞ ) ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → 𝑗 ∈ dom 𝐹 )
14 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
15 14 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑗 ) < +∞ ) ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
16 mnfxr ⊢ -∞ ∈ ℝ*
17 16 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → -∞ ∈ ℝ* )
18 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
19 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → -∞ < ( 𝐹 ‘ 𝑗 ) )
20 17 18 19 xrgtned ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ≠ -∞ )
21 20 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑗 ) < +∞ ) ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ≠ -∞ )
22 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑗 ) < +∞ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
23 pnfxr ⊢ +∞ ∈ ℝ*
24 23 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑗 ) < +∞ ) → +∞ ∈ ℝ* )
25 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑗 ) < +∞ ) → ( 𝐹 ‘ 𝑗 ) < +∞ )
26 22 24 25 xrltned ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑗 ) < +∞ ) → ( 𝐹 ‘ 𝑗 ) ≠ +∞ )
27 26 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑗 ) < +∞ ) ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ≠ +∞ )
28 15 21 27 xrred ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑗 ) < +∞ ) ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
29 13 28 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑗 ) < +∞ ) ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) )
30 29 expl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑗 ) < +∞ ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) ) )
31 6 8 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( ( 𝐹 ‘ 𝑗 ) < +∞ ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) ) )
32 31 ralimdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑗 ) < +∞ ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) ) )
33 32 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑗 ) < +∞ ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) )
34 3 ffund ⊢ ( 𝜑 → Fun 𝐹 )
35 ffvresb ⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ℝ ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) ) )
36 34 35 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ℝ ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) ) )
37 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑗 ) < +∞ ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ℝ ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) ) )
38 33 37 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑗 ) < +∞ ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ℝ )
39 nfv ⊢ Ⅎ 𝑗 𝜑
40 nfcv ⊢ Ⅎ 𝑗 𝐹
41 39 40 1 2 3 4 limsupubuz2 ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) < +∞ )
42 39 40 1 2 3 5 liminflbuz2 ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -∞ < ( 𝐹 ‘ 𝑗 ) )
43 2 rexanuz2 ⊢ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑗 ) < +∞ ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) ↔ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) < +∞ ∧ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -∞ < ( 𝐹 ‘ 𝑗 ) ) )
44 41 42 43 sylanbrc ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑗 ) < +∞ ∧ -∞ < ( 𝐹 ‘ 𝑗 ) ) )
45 38 44 reximddv3 ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ℝ )