| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mnfxr 11319 | . . . . 5
⊢ -∞
∈ ℝ* | 
| 2 | 1 | a1i 11 | . . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → -∞ ∈
ℝ*) | 
| 3 |  | renegcl 11573 | . . . . . 6
⊢ (𝑏 ∈ ℝ → -𝑏 ∈
ℝ) | 
| 4 | 3 | rexrd 11312 | . . . . 5
⊢ (𝑏 ∈ ℝ → -𝑏 ∈
ℝ*) | 
| 5 | 4 | ad2antlr 727 | . . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → -𝑏 ∈ ℝ*) | 
| 6 |  | limsupre.f | . . . . . . 7
⊢ (𝜑 → 𝐹:𝐵⟶ℝ) | 
| 7 |  | reex 11247 | . . . . . . . . 9
⊢ ℝ
∈ V | 
| 8 | 7 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → ℝ ∈
V) | 
| 9 |  | limsupre.1 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ ℝ) | 
| 10 | 8, 9 | ssexd 5323 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ V) | 
| 11 | 6, 10 | fexd 7248 | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ V) | 
| 12 |  | limsupcl 15510 | . . . . . 6
⊢ (𝐹 ∈ V → (lim
sup‘𝐹) ∈
ℝ*) | 
| 13 | 11, 12 | syl 17 | . . . . 5
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ*) | 
| 14 | 13 | ad2antrr 726 | . . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (lim sup‘𝐹) ∈
ℝ*) | 
| 15 | 3 | mnfltd 13167 | . . . . 5
⊢ (𝑏 ∈ ℝ → -∞
< -𝑏) | 
| 16 | 15 | ad2antlr 727 | . . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → -∞ < -𝑏) | 
| 17 | 9 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → 𝐵 ⊆ ℝ) | 
| 18 |  | ressxr 11306 | . . . . . . . 8
⊢ ℝ
⊆ ℝ* | 
| 19 | 18 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℝ*) | 
| 20 | 6, 19 | fssd 6752 | . . . . . 6
⊢ (𝜑 → 𝐹:𝐵⟶ℝ*) | 
| 21 | 20 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → 𝐹:𝐵⟶ℝ*) | 
| 22 |  | limsupre.2 | . . . . . 6
⊢ (𝜑 → sup(𝐵, ℝ*, < ) =
+∞) | 
| 23 | 22 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → sup(𝐵, ℝ*, < ) =
+∞) | 
| 24 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) | 
| 25 |  | nfv 1913 | . . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ 𝑏 ∈ ℝ) | 
| 26 |  | nfre1 3284 | . . . . . . . . 9
⊢
Ⅎ𝑘∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) | 
| 27 | 25, 26 | nfan 1898 | . . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) | 
| 28 |  | nfv 1913 | . . . . . . . . . . . 12
⊢
Ⅎ𝑗(𝜑 ∧ 𝑏 ∈ ℝ) | 
| 29 |  | nfv 1913 | . . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑘 ∈ ℝ | 
| 30 |  | nfra1 3283 | . . . . . . . . . . . 12
⊢
Ⅎ𝑗∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) | 
| 31 | 28, 29, 30 | nf3an 1900 | . . . . . . . . . . 11
⊢
Ⅎ𝑗((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) | 
| 32 |  | simp13 1205 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) | 
| 33 |  | simp2 1137 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → 𝑗 ∈ 𝐵) | 
| 34 |  | simp3 1138 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → 𝑘 ≤ 𝑗) | 
| 35 |  | rspa 3247 | . . . . . . . . . . . . . . . 16
⊢
((∀𝑗 ∈
𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) ∧ 𝑗 ∈ 𝐵) → (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) | 
| 36 | 35 | imp 406 | . . . . . . . . . . . . . . 15
⊢
(((∀𝑗 ∈
𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) ∧ 𝑗 ∈ 𝐵) ∧ 𝑘 ≤ 𝑗) → (abs‘(𝐹‘𝑗)) ≤ 𝑏) | 
| 37 | 32, 33, 34, 36 | syl21anc 837 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → (abs‘(𝐹‘𝑗)) ≤ 𝑏) | 
| 38 |  | simp11l 1284 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → 𝜑) | 
| 39 | 6 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐵) → (𝐹‘𝑗) ∈ ℝ) | 
| 40 | 38, 33, 39 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → (𝐹‘𝑗) ∈ ℝ) | 
| 41 |  | simp11r 1285 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → 𝑏 ∈ ℝ) | 
| 42 | 40, 41 | absled 15470 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → ((abs‘(𝐹‘𝑗)) ≤ 𝑏 ↔ (-𝑏 ≤ (𝐹‘𝑗) ∧ (𝐹‘𝑗) ≤ 𝑏))) | 
| 43 | 37, 42 | mpbid 232 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → (-𝑏 ≤ (𝐹‘𝑗) ∧ (𝐹‘𝑗) ≤ 𝑏)) | 
| 44 | 43 | simpld 494 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → -𝑏 ≤ (𝐹‘𝑗)) | 
| 45 | 44 | 3exp 1119 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (𝑗 ∈ 𝐵 → (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) | 
| 46 | 31, 45 | ralrimi 3256 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))) | 
| 47 | 46 | 3exp 1119 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (𝑘 ∈ ℝ → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))))) | 
| 48 | 47 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (𝑘 ∈ ℝ → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))))) | 
| 49 | 27, 48 | reximdai 3260 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) | 
| 50 | 24, 49 | mpd 15 | . . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))) | 
| 51 |  | breq2 5146 | . . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (ℎ ≤ 𝑖 ↔ ℎ ≤ 𝑗)) | 
| 52 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝐹‘𝑖) = (𝐹‘𝑗)) | 
| 53 | 52 | breq2d 5154 | . . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (-𝑏 ≤ (𝐹‘𝑖) ↔ -𝑏 ≤ (𝐹‘𝑗))) | 
| 54 | 51, 53 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑖 = 𝑗 → ((ℎ ≤ 𝑖 → -𝑏 ≤ (𝐹‘𝑖)) ↔ (ℎ ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) | 
| 55 | 54 | cbvralvw 3236 | . . . . . . . 8
⊢
(∀𝑖 ∈
𝐵 (ℎ ≤ 𝑖 → -𝑏 ≤ (𝐹‘𝑖)) ↔ ∀𝑗 ∈ 𝐵 (ℎ ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))) | 
| 56 |  | breq1 5145 | . . . . . . . . . 10
⊢ (ℎ = 𝑘 → (ℎ ≤ 𝑗 ↔ 𝑘 ≤ 𝑗)) | 
| 57 | 56 | imbi1d 341 | . . . . . . . . 9
⊢ (ℎ = 𝑘 → ((ℎ ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)) ↔ (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) | 
| 58 | 57 | ralbidv 3177 | . . . . . . . 8
⊢ (ℎ = 𝑘 → (∀𝑗 ∈ 𝐵 (ℎ ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)) ↔ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) | 
| 59 | 55, 58 | bitrid 283 | . . . . . . 7
⊢ (ℎ = 𝑘 → (∀𝑖 ∈ 𝐵 (ℎ ≤ 𝑖 → -𝑏 ≤ (𝐹‘𝑖)) ↔ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) | 
| 60 | 59 | cbvrexvw 3237 | . . . . . 6
⊢
(∃ℎ ∈
ℝ ∀𝑖 ∈
𝐵 (ℎ ≤ 𝑖 → -𝑏 ≤ (𝐹‘𝑖)) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))) | 
| 61 | 50, 60 | sylibr 234 | . . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∃ℎ ∈ ℝ ∀𝑖 ∈ 𝐵 (ℎ ≤ 𝑖 → -𝑏 ≤ (𝐹‘𝑖))) | 
| 62 | 17, 21, 5, 23, 61 | limsupbnd2 15520 | . . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → -𝑏 ≤ (lim sup‘𝐹)) | 
| 63 | 2, 5, 14, 16, 62 | xrltletrd 13204 | . . 3
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → -∞ < (lim sup‘𝐹)) | 
| 64 |  | limsupre.bnd | . . 3
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) | 
| 65 | 63, 64 | r19.29a 3161 | . 2
⊢ (𝜑 → -∞ < (lim
sup‘𝐹)) | 
| 66 |  | rexr 11308 | . . . . 5
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℝ*) | 
| 67 | 66 | ad2antlr 727 | . . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → 𝑏 ∈ ℝ*) | 
| 68 |  | pnfxr 11316 | . . . . 5
⊢ +∞
∈ ℝ* | 
| 69 | 68 | a1i 11 | . . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → +∞ ∈
ℝ*) | 
| 70 | 43 | simprd 495 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝑏) | 
| 71 | 70 | 3exp 1119 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (𝑗 ∈ 𝐵 → (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) | 
| 72 | 31, 71 | ralrimi 3256 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)) | 
| 73 | 72 | 3exp 1119 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (𝑘 ∈ ℝ → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)))) | 
| 74 | 73 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (𝑘 ∈ ℝ → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)))) | 
| 75 | 27, 74 | reximdai 3260 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) | 
| 76 | 24, 75 | mpd 15 | . . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)) | 
| 77 | 52 | breq1d 5152 | . . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((𝐹‘𝑖) ≤ 𝑏 ↔ (𝐹‘𝑗) ≤ 𝑏)) | 
| 78 | 51, 77 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑖 = 𝑗 → ((ℎ ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑏) ↔ (ℎ ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) | 
| 79 | 78 | cbvralvw 3236 | . . . . . . . 8
⊢
(∀𝑖 ∈
𝐵 (ℎ ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑏) ↔ ∀𝑗 ∈ 𝐵 (ℎ ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)) | 
| 80 | 56 | imbi1d 341 | . . . . . . . . 9
⊢ (ℎ = 𝑘 → ((ℎ ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏) ↔ (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) | 
| 81 | 80 | ralbidv 3177 | . . . . . . . 8
⊢ (ℎ = 𝑘 → (∀𝑗 ∈ 𝐵 (ℎ ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏) ↔ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) | 
| 82 | 79, 81 | bitrid 283 | . . . . . . 7
⊢ (ℎ = 𝑘 → (∀𝑖 ∈ 𝐵 (ℎ ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑏) ↔ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) | 
| 83 | 82 | cbvrexvw 3237 | . . . . . 6
⊢
(∃ℎ ∈
ℝ ∀𝑖 ∈
𝐵 (ℎ ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑏) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)) | 
| 84 | 76, 83 | sylibr 234 | . . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∃ℎ ∈ ℝ ∀𝑖 ∈ 𝐵 (ℎ ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑏)) | 
| 85 | 17, 21, 67, 84 | limsupbnd1 15519 | . . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (lim sup‘𝐹) ≤ 𝑏) | 
| 86 |  | ltpnf 13163 | . . . . 5
⊢ (𝑏 ∈ ℝ → 𝑏 < +∞) | 
| 87 | 86 | ad2antlr 727 | . . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → 𝑏 < +∞) | 
| 88 | 14, 67, 69, 85, 87 | xrlelttrd 13203 | . . 3
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (lim sup‘𝐹) < +∞) | 
| 89 | 88, 64 | r19.29a 3161 | . 2
⊢ (𝜑 → (lim sup‘𝐹) <
+∞) | 
| 90 |  | xrrebnd 13211 | . . 3
⊢ ((lim
sup‘𝐹) ∈
ℝ* → ((lim sup‘𝐹) ∈ ℝ ↔ (-∞ < (lim
sup‘𝐹) ∧ (lim
sup‘𝐹) <
+∞))) | 
| 91 | 13, 90 | syl 17 | . 2
⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔
(-∞ < (lim sup‘𝐹) ∧ (lim sup‘𝐹) < +∞))) | 
| 92 | 65, 89, 91 | mpbir2and 713 | 1
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ) |