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 ‘ 𝐹 ) ∈ ℝ )