liminfltlem

Description: Given a sequence of real numbers, there exists an upper part of the sequence that's approximated from above by the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfltlem.m	$⊢ φ \to M \in ℤ$
	liminfltlem.z	$⊢ Z = ℤ_{\geq M}$
	liminfltlem.f	$⊢ φ \to F : Z ⟶ ℝ$
	liminfltlem.r	$⊢ φ \to lim inf (F) \in ℝ$
	liminfltlem.x	$⊢ φ \to X \in ℝ^{+}$
Assertion	liminfltlem	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} lim inf (F) < F (k) + X$

Proof

Step	Hyp	Ref	Expression
1		liminfltlem.m	$⊢ φ \to M \in ℤ$
2		liminfltlem.z	$⊢ Z = ℤ_{\geq M}$
3		liminfltlem.f	$⊢ φ \to F : Z ⟶ ℝ$
4		liminfltlem.r	$⊢ φ \to lim inf (F) \in ℝ$
5		liminfltlem.x	$⊢ φ \to X \in ℝ^{+}$
6		nfmpt1	$⊢ \underline{Ⅎ} k (k \in Z ⟼ - F (k))$
7	3	ffvelcdmda	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
8	7	renegcld	$⊢ (φ \land k \in Z) \to - F (k) \in ℝ$
9	8	fmpttd	$⊢ φ \to (k \in Z ⟼ - F (k)) : Z ⟶ ℝ$
10	2	fvexi	$⊢ Z \in V$
11	10	mptex	$⊢ (k \in Z ⟼ - F (k)) \in V$
12	11	limsupcli	$⊢ lim sup ((k \in Z ⟼ - F (k))) \in ℝ^{*}$
13	12	a1i	$⊢ φ \to lim sup ((k \in Z ⟼ - F (k))) \in ℝ^{*}$
14		nfv	$⊢ Ⅎ k φ$
15		nfcv	$⊢ \underline{Ⅎ} k F$
16	14 15 1 2 3	liminfvaluz4	$⊢ φ \to lim inf (F) = - lim sup ((k \in Z ⟼ - F (k)))$
17	16 4	eqeltrrd	$⊢ φ \to - lim sup ((k \in Z ⟼ - F (k))) \in ℝ$
18	13 17	xnegrecl2d	$⊢ φ \to lim sup ((k \in Z ⟼ - F (k))) \in ℝ$
19	6 1 2 9 18 5	limsupgt	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in Z ⟼ - F (k)) (k) - X < lim sup ((k \in Z ⟼ - F (k)))$
20		simpll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to φ$
21	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
22	21	adantll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
23		negex	$⊢ - F (k) \in V$
24		fvmpt4	$⊢ (k \in Z \land - F (k) \in V) \to (k \in Z ⟼ - F (k)) (k) = - F (k)$
25	23 24	mpan2	$⊢ k \in Z \to (k \in Z ⟼ - F (k)) (k) = - F (k)$
26	25	adantl	$⊢ (φ \land k \in Z) \to (k \in Z ⟼ - F (k)) (k) = - F (k)$
27	26	oveq1d	$⊢ (φ \land k \in Z) \to (k \in Z ⟼ - F (k)) (k) - X = - F (k) - X$
28	7	recnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
29	5	rpred	$⊢ φ \to X \in ℝ$
30	29	adantr	$⊢ (φ \land k \in Z) \to X \in ℝ$
31	30	recnd	$⊢ (φ \land k \in Z) \to X \in ℂ$
32	28 31	negdi2d	$⊢ (φ \land k \in Z) \to - (F (k) + X) = - F (k) - X$
33	27 32	eqtr4d	$⊢ (φ \land k \in Z) \to (k \in Z ⟼ - F (k)) (k) - X = - (F (k) + X)$
34	18	recnd	$⊢ φ \to lim sup ((k \in Z ⟼ - F (k))) \in ℂ$
35	18	rexnegd	$⊢ φ \to - lim sup ((k \in Z ⟼ - F (k))) = - lim sup ((k \in Z ⟼ - F (k)))$
36	16 35	eqtr2d	$⊢ φ \to - lim sup ((k \in Z ⟼ - F (k))) = lim inf (F)$
37	34 36	negcon1ad	$⊢ φ \to - lim inf (F) = lim sup ((k \in Z ⟼ - F (k)))$
38	37	eqcomd	$⊢ φ \to lim sup ((k \in Z ⟼ - F (k))) = - lim inf (F)$
39	38	adantr	$⊢ (φ \land k \in Z) \to lim sup ((k \in Z ⟼ - F (k))) = - lim inf (F)$
40	33 39	breq12d	$⊢ (φ \land k \in Z) \to ((k \in Z ⟼ - F (k)) (k) - X < lim sup ((k \in Z ⟼ - F (k))) \leftrightarrow - (F (k) + X) < - lim inf (F))$
41	4	adantr	$⊢ (φ \land k \in Z) \to lim inf (F) \in ℝ$
42	7 30	readdcld	$⊢ (φ \land k \in Z) \to F (k) + X \in ℝ$
43	41 42	ltnegd	$⊢ (φ \land k \in Z) \to (lim inf (F) < F (k) + X \leftrightarrow - (F (k) + X) < - lim inf (F))$
44	40 43	bitr4d	$⊢ (φ \land k \in Z) \to ((k \in Z ⟼ - F (k)) (k) - X < lim sup ((k \in Z ⟼ - F (k))) \leftrightarrow lim inf (F) < F (k) + X)$
45	20 22 44	syl2anc	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to ((k \in Z ⟼ - F (k)) (k) - X < lim sup ((k \in Z ⟼ - F (k))) \leftrightarrow lim inf (F) < F (k) + X)$
46	45	ralbidva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in Z ⟼ - F (k)) (k) - X < lim sup ((k \in Z ⟼ - F (k))) \leftrightarrow \forall k \in ℤ_{\geq j} lim inf (F) < F (k) + X)$
47	46	rexbidva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in Z ⟼ - F (k)) (k) - X < lim sup ((k \in Z ⟼ - F (k))) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} lim inf (F) < F (k) + X)$
48	19 47	mpbid	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} lim inf (F) < F (k) + X$

Metamath Proof Explorer

Theorem liminfltlem

Proof