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

Proof

Step	Hyp	Ref	Expression
1		liminflbuz2.1	$⊢ Ⅎ j φ$
2		liminflbuz2.2	$⊢ \underline{Ⅎ} j F$
3		liminflbuz2.3	$⊢ φ \to M \in ℤ$
4		liminflbuz2.4	$⊢ Z = ℤ_{\geq M}$
5		liminflbuz2.5	$⊢ φ \to F : Z ⟶ ℝ^{*}$
6		liminflbuz2.6	$⊢ φ \to lim inf (F) \neq −∞$
7		nfv	$⊢ Ⅎ j k \in Z$
8	1 7	nfan	$⊢ Ⅎ j (φ \land k \in Z)$
9		simpll	$⊢ ((φ \land k \in Z) \land j \in ℤ_{\geq k}) \to φ$
10	4	uztrn2	$⊢ (k \in Z \land j \in ℤ_{\geq k}) \to j \in Z$
11	10	adantll	$⊢ ((φ \land k \in Z) \land j \in ℤ_{\geq k}) \to j \in Z$
12	5	ffvelrnda	$⊢ (φ \land j \in Z) \to F (j) \in ℝ^{*}$
13	12	adantr	$⊢ ((φ \land j \in Z) \land \neg −∞ < F (j)) \to F (j) \in ℝ^{*}$
14		mnfxr	$⊢ −∞ \in ℝ^{*}$
15	14	a1i	$⊢ ((φ \land j \in Z) \land \neg −∞ < F (j)) \to −∞ \in ℝ^{*}$
16		simpr	$⊢ ((φ \land j \in Z) \land \neg −∞ < F (j)) \to \neg −∞ < F (j)$
17	13 15 16	xrnltled	$⊢ ((φ \land j \in Z) \land \neg −∞ < F (j)) \to F (j) \leq −∞$
18		xlemnf	$⊢ F (j) \in ℝ^{*} \to (F (j) \leq −∞ \leftrightarrow F (j) = −∞)$
19	13 18	syl	$⊢ ((φ \land j \in Z) \land \neg −∞ < F (j)) \to (F (j) \leq −∞ \leftrightarrow F (j) = −∞)$
20	17 19	mpbid	$⊢ ((φ \land j \in Z) \land \neg −∞ < F (j)) \to F (j) = −∞$
21		xnegeq	$⊢ F (j) = −∞ \to - F (j) = - −∞$
22		xnegmnf	$⊢ - −∞ = +∞$
23	21 22	eqtrdi	$⊢ F (j) = −∞ \to - F (j) = +∞$
24	20 23	syl	$⊢ ((φ \land j \in Z) \land \neg −∞ < F (j)) \to - F (j) = +∞$
25	24	adantlr	$⊢ (((φ \land j \in Z) \land - F (j) \neq +∞) \land \neg −∞ < F (j)) \to - F (j) = +∞$
26		neneq	$⊢ - F (j) \neq +∞ \to \neg - F (j) = +∞$
27	26	ad2antlr	$⊢ (((φ \land j \in Z) \land - F (j) \neq +∞) \land \neg −∞ < F (j)) \to \neg - F (j) = +∞$
28	25 27	condan	$⊢ ((φ \land j \in Z) \land - F (j) \neq +∞) \to −∞ < F (j)$
29	28	ex	$⊢ (φ \land j \in Z) \to (- F (j) \neq +∞ \to −∞ < F (j))$
30	9 11 29	syl2anc	$⊢ ((φ \land k \in Z) \land j \in ℤ_{\geq k}) \to (- F (j) \neq +∞ \to −∞ < F (j))$
31	8 30	ralimdaa	$⊢ (φ \land k \in Z) \to (\forall j \in ℤ_{\geq k} - F (j) \neq +∞ \to \forall j \in ℤ_{\geq k} −∞ < F (j))$
32	31	imp	$⊢ ((φ \land k \in Z) \land \forall j \in ℤ_{\geq k} - F (j) \neq +∞) \to \forall j \in ℤ_{\geq k} −∞ < F (j)$
33	12	xnegcld	$⊢ (φ \land j \in Z) \to - F (j) \in ℝ^{*}$
34	33	adantr	$⊢ ((φ \land j \in Z) \land (j \in Z ⟼ - F (j)) (j) < +∞) \to - F (j) \in ℝ^{*}$
35		pnfxr	$⊢ +∞ \in ℝ^{*}$
36	35	a1i	$⊢ ((φ \land j \in Z) \land (j \in Z ⟼ - F (j)) (j) < +∞) \to +∞ \in ℝ^{*}$
37		eqidd	$⊢ φ \to (j \in Z ⟼ - F (j)) = (j \in Z ⟼ - F (j))$
38	37 33	fvmpt2d	$⊢ (φ \land j \in Z) \to (j \in Z ⟼ - F (j)) (j) = - F (j)$
39	38	adantr	$⊢ ((φ \land j \in Z) \land (j \in Z ⟼ - F (j)) (j) < +∞) \to (j \in Z ⟼ - F (j)) (j) = - F (j)$
40		simpr	$⊢ ((φ \land j \in Z) \land (j \in Z ⟼ - F (j)) (j) < +∞) \to (j \in Z ⟼ - F (j)) (j) < +∞$
41	39 40	eqbrtrrd	$⊢ ((φ \land j \in Z) \land (j \in Z ⟼ - F (j)) (j) < +∞) \to - F (j) < +∞$
42	34 36 41	xrltned	$⊢ ((φ \land j \in Z) \land (j \in Z ⟼ - F (j)) (j) < +∞) \to - F (j) \neq +∞$
43	42	ex	$⊢ (φ \land j \in Z) \to ((j \in Z ⟼ - F (j)) (j) < +∞ \to - F (j) \neq +∞)$
44	9 11 43	syl2anc	$⊢ ((φ \land k \in Z) \land j \in ℤ_{\geq k}) \to ((j \in Z ⟼ - F (j)) (j) < +∞ \to - F (j) \neq +∞)$
45	8 44	ralimdaa	$⊢ (φ \land k \in Z) \to (\forall j \in ℤ_{\geq k} (j \in Z ⟼ - F (j)) (j) < +∞ \to \forall j \in ℤ_{\geq k} - F (j) \neq +∞)$
46	45	imp	$⊢ ((φ \land k \in Z) \land \forall j \in ℤ_{\geq k} (j \in Z ⟼ - F (j)) (j) < +∞) \to \forall j \in ℤ_{\geq k} - F (j) \neq +∞$
47		nfmpt1	$⊢ \underline{Ⅎ} j (j \in Z ⟼ - F (j))$
48	1 33	fmptd2f	$⊢ φ \to (j \in Z ⟼ - F (j)) : Z ⟶ ℝ^{*}$
49	4	fvexi	$⊢ Z \in V$
50	49	a1i	$⊢ φ \to Z \in V$
51	5 50	fexd	$⊢ φ \to F \in V$
52	51	liminfcld	$⊢ φ \to lim inf (F) \in ℝ^{*}$
53	52	xnegnegd	$⊢ φ \to - (- lim inf (F)) = lim inf (F)$
54	1 2 3 4 5	liminfvaluz3	$⊢ φ \to lim inf (F) = - lim sup ((j \in Z ⟼ - F (j)))$
55	53 54	eqtr2d	$⊢ φ \to - lim sup ((j \in Z ⟼ - F (j))) = - (- lim inf (F))$
56	50	mptexd	$⊢ φ \to (j \in Z ⟼ - F (j)) \in V$
57	56	limsupcld	$⊢ φ \to lim sup ((j \in Z ⟼ - F (j))) \in ℝ^{*}$
58	52	xnegcld	$⊢ φ \to - lim inf (F) \in ℝ^{*}$
59		xneg11	$⊢ (lim sup ((j \in Z ⟼ - F (j))) \in ℝ^{} \land - lim inf (F) \in ℝ^{}) \to (- lim sup ((j \in Z ⟼ - F (j))) = - (- lim inf (F)) \leftrightarrow lim sup ((j \in Z ⟼ - F (j))) = - lim inf (F))$
60	57 58 59	syl2anc	$⊢ φ \to (- lim sup ((j \in Z ⟼ - F (j))) = - (- lim inf (F)) \leftrightarrow lim sup ((j \in Z ⟼ - F (j))) = - lim inf (F))$
61	55 60	mpbid	$⊢ φ \to lim sup ((j \in Z ⟼ - F (j))) = - lim inf (F)$
62		nne	$⊢ \neg - lim inf (F) \neq +∞ \leftrightarrow - lim inf (F) = +∞$
63	53	eqcomd	$⊢ φ \to lim inf (F) = - (- lim inf (F))$
64	63	adantr	$⊢ (φ \land - lim inf (F) = +∞) \to lim inf (F) = - (- lim inf (F))$
65		xnegeq	$⊢ - lim inf (F) = +∞ \to - (- lim inf (F)) = - +∞$
66	65	adantl	$⊢ (φ \land - lim inf (F) = +∞) \to - (- lim inf (F)) = - +∞$
67		xnegpnf	$⊢ - +∞ = −∞$
68	67	a1i	$⊢ (φ \land - lim inf (F) = +∞) \to - +∞ = −∞$
69	64 66 68	3eqtrd	$⊢ (φ \land - lim inf (F) = +∞) \to lim inf (F) = −∞$
70	62 69	sylan2b	$⊢ (φ \land \neg - lim inf (F) \neq +∞) \to lim inf (F) = −∞$
71	6	neneqd	$⊢ φ \to \neg lim inf (F) = −∞$
72	71	adantr	$⊢ (φ \land \neg - lim inf (F) \neq +∞) \to \neg lim inf (F) = −∞$
73	70 72	condan	$⊢ φ \to - lim inf (F) \neq +∞$
74	61 73	eqnetrd	$⊢ φ \to lim sup ((j \in Z ⟼ - F (j))) \neq +∞$
75	1 47 3 4 48 74	limsupubuz2	$⊢ φ \to \exists k \in Z \forall j \in ℤ_{\geq k} (j \in Z ⟼ - F (j)) (j) < +∞$
76	46 75	reximddv3	$⊢ φ \to \exists k \in Z \forall j \in ℤ_{\geq k} - F (j) \neq +∞$
77	32 76	reximddv3	$⊢ φ \to \exists k \in Z \forall j \in ℤ_{\geq k} −∞ < F (j)$

Metamath Proof Explorer

Theorem liminflbuz2

Proof