Metamath Proof Explorer

Theorem limsupre

Description: If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypotheses limsupre.1 ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
limsupre.2 ⊢ ( 𝜑 → sup ( 𝐵 , ℝ* , < ) = +∞ )
limsupre.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ )
limsupre.bnd ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) )
Assertion limsupre ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 limsupre.1 ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
2 limsupre.2 ⊢ ( 𝜑 → sup ( 𝐵 , ℝ* , < ) = +∞ )
3 limsupre.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ )
4 limsupre.bnd ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) )
5 mnfxr ⊢ -∞ ∈ ℝ*
6 5 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → -∞ ∈ ℝ* )
7 renegcl ⊢ ( 𝑏 ∈ ℝ → - 𝑏 ∈ ℝ )
8 7 rexrd ⊢ ( 𝑏 ∈ ℝ → - 𝑏 ∈ ℝ* )
9 8 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → - 𝑏 ∈ ℝ* )
10 reex ⊢ ℝ ∈ V
11 10 a1i ⊢ ( 𝜑 → ℝ ∈ V )
12 11 1 ssexd ⊢ ( 𝜑 → 𝐵 ∈ V )
13 3 12 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
14 limsupcl ⊢ ( 𝐹 ∈ V → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
15 13 14 syl ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
16 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
17 7 mnfltd ⊢ ( 𝑏 ∈ ℝ → -∞ < - 𝑏 )
18 17 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → -∞ < - 𝑏 )
19 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → 𝐵 ⊆ ℝ )
20 ressxr ⊢ ℝ ⊆ ℝ*
21 20 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ* )
22 3 21 fssd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → 𝐹 : 𝐵 ⟶ ℝ* )
24 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → sup ( 𝐵 , ℝ* , < ) = +∞ )
25 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) )
26 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑏 ∈ ℝ )
27 nfre1 ⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 )
28 26 27 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) )
29 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑏 ∈ ℝ )
30 nfv ⊢ Ⅎ 𝑗 𝑘 ∈ ℝ
31 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 )
32 29 30 31 nf3an ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) )
33 simp13 ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) )
34 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ 𝐵 )
35 simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → 𝑘 ≤ 𝑗 )
36 rspa ⊢ ( ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ∧ 𝑗 ∈ 𝐵 ) → ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) )
37 36 imp ⊢ ( ( ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑘 ≤ 𝑗 ) → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 )
38 33 34 35 37 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 )
39 simp11l ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → 𝜑 )
40 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
41 39 34 40 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
42 simp11r ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → 𝑏 ∈ ℝ )
43 41 42 absled ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ↔ ( - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ) )
44 38 43 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → ( - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) )
45 44 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) )
46 45 3exp ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ( 𝑗 ∈ 𝐵 → ( 𝑘 ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
47 32 46 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) )
48 47 3exp ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → ( 𝑘 ∈ ℝ → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) → ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) )
49 48 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ( 𝑘 ∈ ℝ → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) → ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) )
50 28 49 reximdai ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
51 25 50 mpd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) )
52 breq2 ⊢ ( 𝑖 = 𝑗 → ( ℎ ≤ 𝑖 ↔ ℎ ≤ 𝑗 ) )
53 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) )
54 53 breq2d ⊢ ( 𝑖 = 𝑗 → ( - 𝑏 ≤ ( 𝐹 ‘ 𝑖 ) ↔ - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) )
55 52 54 imbi12d ⊢ ( 𝑖 = 𝑗 → ( ( ℎ ≤ 𝑖 → - 𝑏 ≤ ( 𝐹 ‘ 𝑖 ) ) ↔ ( ℎ ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
56 55 cbvralvw ⊢ ( ∀ 𝑖 ∈ 𝐵 ( ℎ ≤ 𝑖 → - 𝑏 ≤ ( 𝐹 ‘ 𝑖 ) ) ↔ ∀ 𝑗 ∈ 𝐵 ( ℎ ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) )
57 breq1 ⊢ ( ℎ = 𝑘 → ( ℎ ≤ 𝑗 ↔ 𝑘 ≤ 𝑗 ) )
58 57 imbi1d ⊢ ( ℎ = 𝑘 → ( ( ℎ ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝑘 ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
59 58 ralbidv ⊢ ( ℎ = 𝑘 → ( ∀ 𝑗 ∈ 𝐵 ( ℎ ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
60 56 59 syl5bb ⊢ ( ℎ = 𝑘 → ( ∀ 𝑖 ∈ 𝐵 ( ℎ ≤ 𝑖 → - 𝑏 ≤ ( 𝐹 ‘ 𝑖 ) ) ↔ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
61 60 cbvrexvw ⊢ ( ∃ ℎ ∈ ℝ ∀ 𝑖 ∈ 𝐵 ( ℎ ≤ 𝑖 → - 𝑏 ≤ ( 𝐹 ‘ 𝑖 ) ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → - 𝑏 ≤ ( 𝐹 ‘ 𝑗 ) ) )
62 51 61 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ∃ ℎ ∈ ℝ ∀ 𝑖 ∈ 𝐵 ( ℎ ≤ 𝑖 → - 𝑏 ≤ ( 𝐹 ‘ 𝑖 ) ) )
63 19 23 9 24 62 limsupbnd2 ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → - 𝑏 ≤ ( lim sup ‘ 𝐹 ) )
64 6 9 16 18 63 xrltletrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → -∞ < ( lim sup ‘ 𝐹 ) )
65 64 4 r19.29a ⊢ ( 𝜑 → -∞ < ( lim sup ‘ 𝐹 ) )
66 rexr ⊢ ( 𝑏 ∈ ℝ → 𝑏 ∈ ℝ* )
67 66 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → 𝑏 ∈ ℝ* )
68 pnfxr ⊢ +∞ ∈ ℝ*
69 68 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → +∞ ∈ ℝ* )
70 44 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 )
71 70 3exp ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ( 𝑗 ∈ 𝐵 → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ) )
72 32 71 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) )
73 72 3exp ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → ( 𝑘 ∈ ℝ → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) → ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ) ) )
74 73 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ( 𝑘 ∈ ℝ → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) → ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ) ) )
75 28 74 reximdai ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ) )
76 25 75 mpd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) )
77 53 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑏 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) )
78 52 77 imbi12d ⊢ ( 𝑖 = 𝑗 → ( ( ℎ ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑏 ) ↔ ( ℎ ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ) )
79 78 cbvralvw ⊢ ( ∀ 𝑖 ∈ 𝐵 ( ℎ ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑏 ) ↔ ∀ 𝑗 ∈ 𝐵 ( ℎ ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) )
80 57 imbi1d ⊢ ( ℎ = 𝑘 → ( ( ℎ ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ↔ ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ) )
81 80 ralbidv ⊢ ( ℎ = 𝑘 → ( ∀ 𝑗 ∈ 𝐵 ( ℎ ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ↔ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ) )
82 79 81 syl5bb ⊢ ( ℎ = 𝑘 → ( ∀ 𝑖 ∈ 𝐵 ( ℎ ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑏 ) ↔ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) ) )
83 82 cbvrexvw ⊢ ( ∃ ℎ ∈ ℝ ∀ 𝑖 ∈ 𝐵 ( ℎ ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑏 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 ) )
84 76 83 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ∃ ℎ ∈ ℝ ∀ 𝑖 ∈ 𝐵 ( ℎ ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑏 ) )
85 19 23 67 84 limsupbnd1 ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ( lim sup ‘ 𝐹 ) ≤ 𝑏 )
86 ltpnf ⊢ ( 𝑏 ∈ ℝ → 𝑏 < +∞ )
87 86 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → 𝑏 < +∞ )
88 16 67 69 85 87 xrlelttrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ( lim sup ‘ 𝐹 ) < +∞ )
89 88 4 r19.29a ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) < +∞ )
90 xrrebnd ⊢ ( ( lim sup ‘ 𝐹 ) ∈ ℝ* → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( -∞ < ( lim sup ‘ 𝐹 ) ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ) )
91 15 90 syl ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( -∞ < ( lim sup ‘ 𝐹 ) ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ) )
92 65 89 91 mpbir2and ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )