This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupref

Description: If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupref.j ⊢ Ⅎ 𝑗 𝐹
limsupref.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limsupref.s ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
limsupref.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
limsupref.b ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) )
Assertion limsupref ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 limsupref.j ⊢ Ⅎ 𝑗 𝐹
2 limsupref.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 limsupref.s ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
4 limsupref.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
5 limsupref.b ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) )
6 breq2 ⊢ ( 𝑏 = 𝑦 → ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) )
7 6 imbi2d ⊢ ( 𝑏 = 𝑦 → ( ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ↔ ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) ) )
8 7 ralbidv ⊢ ( 𝑏 = 𝑦 → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) ) )
9 breq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ≤ 𝑗 ↔ 𝑖 ≤ 𝑗 ) )
10 9 imbi1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) ↔ ( 𝑖 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) ) )
11 10 ralbidv ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑖 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) ) )
12 nfv ⊢ Ⅎ 𝑥 ( 𝑖 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 )
13 nfv ⊢ Ⅎ 𝑗 𝑖 ≤ 𝑥
14 nfcv ⊢ Ⅎ 𝑗 abs
15 nfcv ⊢ Ⅎ 𝑗 𝑥
16 1 15 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑥 )
17 14 16 nffv ⊢ Ⅎ 𝑗 ( abs ‘ ( 𝐹 ‘ 𝑥 ) )
18 nfcv ⊢ Ⅎ 𝑗 ≤
19 nfcv ⊢ Ⅎ 𝑗 𝑦
20 17 18 19 nfbr ⊢ Ⅎ 𝑗 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦
21 13 20 nfim ⊢ Ⅎ 𝑗 ( 𝑖 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
22 breq2 ⊢ ( 𝑗 = 𝑥 → ( 𝑖 ≤ 𝑗 ↔ 𝑖 ≤ 𝑥 ) )
23 2fveq3 ⊢ ( 𝑗 = 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
24 23 breq1d ⊢ ( 𝑗 = 𝑥 → ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ↔ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
25 22 24 imbi12d ⊢ ( 𝑗 = 𝑥 → ( ( 𝑖 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) ↔ ( 𝑖 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
26 12 21 25 cbvralw ⊢ ( ∀ 𝑗 ∈ 𝐴 ( 𝑖 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑖 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
27 26 a1i ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ 𝐴 ( 𝑖 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑖 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
28 11 27 bitrd ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑖 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
29 8 28 cbvrex2vw ⊢ ( ∃ 𝑏 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑖 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
30 5 29 sylib ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑖 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
31 2 3 4 30 limsupre ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )