Metamath Proof Explorer

Theorem liminflt

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

Proof

Step Hyp Ref Expression
1 liminflt.k ⊢ Ⅎ 𝑘 𝐹
2 liminflt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 liminflt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 liminflt.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
5 liminflt.r ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ )
6 liminflt.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
7 2 3 4 5 6 liminfltlem ⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑙 ) + 𝑋 ) )
8 fveq2 ⊢ ( 𝑖 = 𝑗 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑗 ) )
9 8 raleqdv ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑙 ) + 𝑋 ) ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑙 ) + 𝑋 ) ) )
10 nfcv ⊢ Ⅎ 𝑘 lim inf
11 10 1 nffv ⊢ Ⅎ 𝑘 ( lim inf ‘ 𝐹 )
12 nfcv ⊢ Ⅎ 𝑘 <
13 nfcv ⊢ Ⅎ 𝑘 𝑙
14 1 13 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 )
15 nfcv ⊢ Ⅎ 𝑘 +
16 nfcv ⊢ Ⅎ 𝑘 𝑋
17 14 15 16 nfov ⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑙 ) + 𝑋 )
18 11 12 17 nfbr ⊢ Ⅎ 𝑘 ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑙 ) + 𝑋 )
19 nfv ⊢ Ⅎ 𝑙 ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 )
20 fveq2 ⊢ ( 𝑙 = 𝑘 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑘 ) )
21 20 oveq1d ⊢ ( 𝑙 = 𝑘 → ( ( 𝐹 ‘ 𝑙 ) + 𝑋 ) = ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) )
22 21 breq2d ⊢ ( 𝑙 = 𝑘 → ( ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑙 ) + 𝑋 ) ↔ ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) ) )
23 18 19 22 cbvralw ⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑙 ) + 𝑋 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) )
24 23 a1i ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑙 ) + 𝑋 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) ) )
25 9 24 bitrd ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑙 ) + 𝑋 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) ) )
26 25 cbvrexvw ⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑙 ) + 𝑋 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) )
27 7 26 sylib ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑋 ) )