Metamath Proof Explorer

Theorem limsupgt

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

Ref Expression
Hypotheses limsupgt.k ⊢ Ⅎ 𝑘 𝐹
limsupgt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
limsupgt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
limsupgt.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
limsupgt.r ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
limsupgt.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
Assertion limsupgt ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) − 𝑋 ) < ( lim sup ‘ 𝐹 ) )

Proof

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