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	⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ℝ )