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