Metamath Proof Explorer

Theorem 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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
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 ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) )