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	$⊢ φ \to M \in ℤ$
	liminflimsupxrre.2	$⊢ Z = ℤ_{\geq M}$
	liminflimsupxrre.3	$⊢ φ \to F : Z ⟶ ℝ^{*}$
	liminflimsupxrre.4	$⊢ φ \to lim sup (F) \neq +∞$
	liminflimsupxrre.5	$⊢ φ \to lim inf (F) \neq −∞$
Assertion	liminflimsupxrre	$⊢ φ \to \exists k \in Z ({F ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		liminflimsupxrre.1	$⊢ φ \to M \in ℤ$
2		liminflimsupxrre.2	$⊢ Z = ℤ_{\geq M}$
3		liminflimsupxrre.3	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		liminflimsupxrre.4	$⊢ φ \to lim sup (F) \neq +∞$
5		liminflimsupxrre.5	$⊢ φ \to lim inf (F) \neq −∞$
6		simpll	$⊢ ((φ \land k \in Z) \land j \in ℤ_{\geq k}) \to φ$
7	2	uztrn2	$⊢ (k \in Z \land j \in ℤ_{\geq k}) \to j \in Z$
8	7	adantll	$⊢ ((φ \land k \in Z) \land j \in ℤ_{\geq k}) \to j \in Z$
9		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
10	3	fdmd	$⊢ φ \to dom F = Z$
11	10	adantr	$⊢ (φ \land j \in Z) \to dom F = Z$
12	9 11	eleqtrrd	$⊢ (φ \land j \in Z) \to j \in dom F$
13	12	ad2antrr	$⊢ (((φ \land j \in Z) \land F (j) < +∞) \land −∞ < F (j)) \to j \in dom F$
14	3	ffvelrnda	$⊢ (φ \land j \in Z) \to F (j) \in ℝ^{*}$
15	14	ad2antrr	$⊢ (((φ \land j \in Z) \land F (j) < +∞) \land −∞ < F (j)) \to F (j) \in ℝ^{*}$
16		mnfxr	$⊢ −∞ \in ℝ^{*}$
17	16	a1i	$⊢ ((φ \land j \in Z) \land −∞ < F (j)) \to −∞ \in ℝ^{*}$
18	14	adantr	$⊢ ((φ \land j \in Z) \land −∞ < F (j)) \to F (j) \in ℝ^{*}$
19		simpr	$⊢ ((φ \land j \in Z) \land −∞ < F (j)) \to −∞ < F (j)$
20	17 18 19	xrgtned	$⊢ ((φ \land j \in Z) \land −∞ < F (j)) \to F (j) \neq −∞$
21	20	adantlr	$⊢ (((φ \land j \in Z) \land F (j) < +∞) \land −∞ < F (j)) \to F (j) \neq −∞$
22	14	adantr	$⊢ ((φ \land j \in Z) \land F (j) < +∞) \to F (j) \in ℝ^{*}$
23		pnfxr	$⊢ +∞ \in ℝ^{*}$
24	23	a1i	$⊢ ((φ \land j \in Z) \land F (j) < +∞) \to +∞ \in ℝ^{*}$
25		simpr	$⊢ ((φ \land j \in Z) \land F (j) < +∞) \to F (j) < +∞$
26	22 24 25	xrltned	$⊢ ((φ \land j \in Z) \land F (j) < +∞) \to F (j) \neq +∞$
27	26	adantr	$⊢ (((φ \land j \in Z) \land F (j) < +∞) \land −∞ < F (j)) \to F (j) \neq +∞$
28	15 21 27	xrred	$⊢ (((φ \land j \in Z) \land F (j) < +∞) \land −∞ < F (j)) \to F (j) \in ℝ$
29	13 28	jca	$⊢ (((φ \land j \in Z) \land F (j) < +∞) \land −∞ < F (j)) \to (j \in dom F \land F (j) \in ℝ)$
30	29	expl	$⊢ (φ \land j \in Z) \to ((F (j) < +∞ \land −∞ < F (j)) \to (j \in dom F \land F (j) \in ℝ))$
31	6 8 30	syl2anc	$⊢ ((φ \land k \in Z) \land j \in ℤ_{\geq k}) \to ((F (j) < +∞ \land −∞ < F (j)) \to (j \in dom F \land F (j) \in ℝ))$
32	31	ralimdva	$⊢ (φ \land k \in Z) \to (\forall j \in ℤ_{\geq k} (F (j) < +∞ \land −∞ < F (j)) \to \forall j \in ℤ_{\geq k} (j \in dom F \land F (j) \in ℝ))$
33	32	imp	$⊢ ((φ \land k \in Z) \land \forall j \in ℤ_{\geq k} (F (j) < +∞ \land −∞ < F (j))) \to \forall j \in ℤ_{\geq k} (j \in dom F \land F (j) \in ℝ)$
34	3	ffund	$⊢ φ \to Fun F$
35		ffvresb	$⊢ Fun F \to (({F ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ ℝ \leftrightarrow \forall j \in ℤ_{\geq k} (j \in dom F \land F (j) \in ℝ))$
36	34 35	syl	$⊢ φ \to (({F ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ ℝ \leftrightarrow \forall j \in ℤ_{\geq k} (j \in dom F \land F (j) \in ℝ))$
37	36	ad2antrr	$⊢ ((φ \land k \in Z) \land \forall j \in ℤ_{\geq k} (F (j) < +∞ \land −∞ < F (j))) \to (({F ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ ℝ \leftrightarrow \forall j \in ℤ_{\geq k} (j \in dom F \land F (j) \in ℝ))$
38	33 37	mpbird	$⊢ ((φ \land k \in Z) \land \forall j \in ℤ_{\geq k} (F (j) < +∞ \land −∞ < F (j))) \to ({F ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ ℝ$
39		nfv	$⊢ Ⅎ j φ$
40		nfcv	$⊢ \underline{Ⅎ} j F$
41	39 40 1 2 3 4	limsupubuz2	$⊢ φ \to \exists k \in Z \forall j \in ℤ_{\geq k} F (j) < +∞$
42	39 40 1 2 3 5	liminflbuz2	$⊢ φ \to \exists k \in Z \forall j \in ℤ_{\geq k} −∞ < F (j)$
43	2	rexanuz2	$⊢ \exists k \in Z \forall j \in ℤ_{\geq k} (F (j) < +∞ \land −∞ < F (j)) \leftrightarrow (\exists k \in Z \forall j \in ℤ_{\geq k} F (j) < +∞ \land \exists k \in Z \forall j \in ℤ_{\geq k} −∞ < F (j))$
44	41 42 43	sylanbrc	$⊢ φ \to \exists k \in Z \forall j \in ℤ_{\geq k} (F (j) < +∞ \land −∞ < F (j))$
45	38 44	reximddv3	$⊢ φ \to \exists k \in Z ({F ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ ℝ$

Metamath Proof Explorer

Theorem liminflimsupxrre

Proof