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	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	liminfltlem.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	liminfltlem.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
	liminfltlem.r	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ )
	liminfltlem.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ⁺ )
Assertion	liminfltlem	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		liminfltlem.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		liminfltlem.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
3		liminfltlem.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4		liminfltlem.r	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ )
5		liminfltlem.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ⁺ )
6		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) )
7	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
8	7	renegcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
9	8	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) : 𝑍 ⟶ ℝ )
10	2	fvexi	⊢ 𝑍 ∈ V
11	10	mptex	⊢ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ∈ V
12	11	limsupcli	⊢ ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ^*
13	12	a1i	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ^* )
14		nfv	⊢ Ⅎ 𝑘 𝜑
15		nfcv	⊢ Ⅎ 𝑘 𝐹
16	14 15 1 2 3	liminfvaluz4	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -_𝑒 ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) )
17	16 4	eqeltrrd	⊢ ( 𝜑 → -_𝑒 ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
18	13 17	xnegrecl2d	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
19	6 1 2 9 18 5	limsupgt	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) − 𝑋 ) < ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) )
20		simpll	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝜑 )
21	2	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
22	21	adantll	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
23		negex	⊢ - ( 𝐹 ‘ 𝑘 ) ∈ V
24		fvmpt4	⊢ ( ( 𝑘 ∈ 𝑍 ∧ - ( 𝐹 ‘ 𝑘 ) ∈ V ) → ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) = - ( 𝐹 ‘ 𝑘 ) )
25	23 24	mpan2	⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) = - ( 𝐹 ‘ 𝑘 ) )
26	25	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) = - ( 𝐹 ‘ 𝑘 ) )
27	26	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) − 𝑋 ) = ( - ( 𝐹 ‘ 𝑘 ) − 𝑋 ) )
28	7	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
29	5	rpred	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑋 ∈ ℝ )
31	30	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑋 ∈ ℂ )
32	28 31	negdi2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) = ( - ( 𝐹 ‘ 𝑘 ) − 𝑋 ) )
33	27 32	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) − 𝑋 ) = - ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) )
34	18	recnd	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℂ )
35	18	rexnegd	⊢ ( 𝜑 → -_𝑒 ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) = - ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) )
36	16 35	eqtr2d	⊢ ( 𝜑 → - ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) = ( lim inf ‘ 𝐹 ) )
37	34 36	negcon1ad	⊢ ( 𝜑 → - ( lim inf ‘ 𝐹 ) = ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) )
38	37	eqcomd	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) = - ( lim inf ‘ 𝐹 ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) = - ( lim inf ‘ 𝐹 ) )
40	33 39	breq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) − 𝑋 ) < ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ↔ - ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) < - ( lim inf ‘ 𝐹 ) ) )
41	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( lim inf ‘ 𝐹 ) ∈ ℝ )
42	7 30	readdcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) ∈ ℝ )
43	41 42	ltnegd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) ↔ - ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) < - ( lim inf ‘ 𝐹 ) ) )
44	40 43	bitr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) − 𝑋 ) < ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ↔ ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) ) )
45	20 22 44	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( ( ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) − 𝑋 ) < ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ↔ ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) ) )
46	45	ralbidva	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) − 𝑋 ) < ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ↔ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) ) )
47	46	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) − 𝑋 ) < ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) ) )
48	19 47	mpbid	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) )

Metamath Proof Explorer

Theorem liminfltlem

Proof