Step | Hyp | Ref
| Expression |
1 | | mnfxr 10534 |
. . . . 5
⊢ -∞
∈ ℝ* |
2 | 1 | a1i 11 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → -∞ ∈
ℝ*) |
3 | | renegcl 10786 |
. . . . . 6
⊢ (𝑏 ∈ ℝ → -𝑏 ∈
ℝ) |
4 | 3 | rexrd 10526 |
. . . . 5
⊢ (𝑏 ∈ ℝ → -𝑏 ∈
ℝ*) |
5 | 4 | ad2antlr 723 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → -𝑏 ∈ ℝ*) |
6 | | limsupre.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐵⟶ℝ) |
7 | | reex 10463 |
. . . . . . . . 9
⊢ ℝ
∈ V |
8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈
V) |
9 | | limsupre.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
10 | 8, 9 | ssexd 5112 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ V) |
11 | | fex 6846 |
. . . . . . 7
⊢ ((𝐹:𝐵⟶ℝ ∧ 𝐵 ∈ V) → 𝐹 ∈ V) |
12 | 6, 10, 11 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ V) |
13 | | limsupcl 14652 |
. . . . . 6
⊢ (𝐹 ∈ V → (lim
sup‘𝐹) ∈
ℝ*) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ*) |
15 | 14 | ad2antrr 722 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (lim sup‘𝐹) ∈
ℝ*) |
16 | 3 | mnfltd 12358 |
. . . . 5
⊢ (𝑏 ∈ ℝ → -∞
< -𝑏) |
17 | 16 | ad2antlr 723 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → -∞ < -𝑏) |
18 | 9 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → 𝐵 ⊆ ℝ) |
19 | | ressxr 10520 |
. . . . . . . 8
⊢ ℝ
⊆ ℝ* |
20 | 19 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℝ*) |
21 | 6, 20 | fssd 6388 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐵⟶ℝ*) |
22 | 21 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → 𝐹:𝐵⟶ℝ*) |
23 | | limsupre.2 |
. . . . . 6
⊢ (𝜑 → sup(𝐵, ℝ*, < ) =
+∞) |
24 | 23 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → sup(𝐵, ℝ*, < ) =
+∞) |
25 | | simpr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) |
26 | | nfv 1890 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ 𝑏 ∈ ℝ) |
27 | | nfre1 3266 |
. . . . . . . . 9
⊢
Ⅎ𝑘∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) |
28 | 26, 27 | nfan 1879 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) |
29 | | nfv 1890 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗(𝜑 ∧ 𝑏 ∈ ℝ) |
30 | | nfv 1890 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑘 ∈ ℝ |
31 | | nfra1 3184 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) |
32 | 29, 30, 31 | nf3an 1881 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) |
33 | | simp13 1196 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) |
34 | | simp2 1128 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → 𝑗 ∈ 𝐵) |
35 | | simp3 1129 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → 𝑘 ≤ 𝑗) |
36 | | rspa 3171 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑗 ∈
𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) ∧ 𝑗 ∈ 𝐵) → (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) |
37 | 36 | imp 407 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑗 ∈
𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) ∧ 𝑗 ∈ 𝐵) ∧ 𝑘 ≤ 𝑗) → (abs‘(𝐹‘𝑗)) ≤ 𝑏) |
38 | 33, 34, 35, 37 | syl21anc 834 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → (abs‘(𝐹‘𝑗)) ≤ 𝑏) |
39 | | simp11l 1275 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → 𝜑) |
40 | 6 | ffvelrnda 6707 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐵) → (𝐹‘𝑗) ∈ ℝ) |
41 | 39, 34, 40 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → (𝐹‘𝑗) ∈ ℝ) |
42 | | simp11r 1276 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → 𝑏 ∈ ℝ) |
43 | 41, 42 | absled 14612 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → ((abs‘(𝐹‘𝑗)) ≤ 𝑏 ↔ (-𝑏 ≤ (𝐹‘𝑗) ∧ (𝐹‘𝑗) ≤ 𝑏))) |
44 | 38, 43 | mpbid 233 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → (-𝑏 ≤ (𝐹‘𝑗) ∧ (𝐹‘𝑗) ≤ 𝑏)) |
45 | 44 | simpld 495 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → -𝑏 ≤ (𝐹‘𝑗)) |
46 | 45 | 3exp 1110 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (𝑗 ∈ 𝐵 → (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) |
47 | 32, 46 | ralrimi 3181 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))) |
48 | 47 | 3exp 1110 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (𝑘 ∈ ℝ → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))))) |
49 | 48 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (𝑘 ∈ ℝ → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))))) |
50 | 28, 49 | reximdai 3269 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) |
51 | 25, 50 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))) |
52 | | breq2 4960 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (ℎ ≤ 𝑖 ↔ ℎ ≤ 𝑗)) |
53 | | fveq2 6530 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝐹‘𝑖) = (𝐹‘𝑗)) |
54 | 53 | breq2d 4968 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (-𝑏 ≤ (𝐹‘𝑖) ↔ -𝑏 ≤ (𝐹‘𝑗))) |
55 | 52, 54 | imbi12d 346 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → ((ℎ ≤ 𝑖 → -𝑏 ≤ (𝐹‘𝑖)) ↔ (ℎ ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) |
56 | 55 | cbvralv 3400 |
. . . . . . . 8
⊢
(∀𝑖 ∈
𝐵 (ℎ ≤ 𝑖 → -𝑏 ≤ (𝐹‘𝑖)) ↔ ∀𝑗 ∈ 𝐵 (ℎ ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))) |
57 | | breq1 4959 |
. . . . . . . . . 10
⊢ (ℎ = 𝑘 → (ℎ ≤ 𝑗 ↔ 𝑘 ≤ 𝑗)) |
58 | 57 | imbi1d 343 |
. . . . . . . . 9
⊢ (ℎ = 𝑘 → ((ℎ ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)) ↔ (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) |
59 | 58 | ralbidv 3162 |
. . . . . . . 8
⊢ (ℎ = 𝑘 → (∀𝑗 ∈ 𝐵 (ℎ ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)) ↔ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) |
60 | 56, 59 | syl5bb 284 |
. . . . . . 7
⊢ (ℎ = 𝑘 → (∀𝑖 ∈ 𝐵 (ℎ ≤ 𝑖 → -𝑏 ≤ (𝐹‘𝑖)) ↔ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗)))) |
61 | 60 | cbvrexv 3401 |
. . . . . 6
⊢
(∃ℎ ∈
ℝ ∀𝑖 ∈
𝐵 (ℎ ≤ 𝑖 → -𝑏 ≤ (𝐹‘𝑖)) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → -𝑏 ≤ (𝐹‘𝑗))) |
62 | 51, 61 | sylibr 235 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∃ℎ ∈ ℝ ∀𝑖 ∈ 𝐵 (ℎ ≤ 𝑖 → -𝑏 ≤ (𝐹‘𝑖))) |
63 | 18, 22, 5, 24, 62 | limsupbnd2 14662 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → -𝑏 ≤ (lim sup‘𝐹)) |
64 | 2, 5, 15, 17, 63 | xrltletrd 12393 |
. . 3
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → -∞ < (lim sup‘𝐹)) |
65 | | limsupre.bnd |
. . 3
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) |
66 | 64, 65 | r19.29a 3249 |
. 2
⊢ (𝜑 → -∞ < (lim
sup‘𝐹)) |
67 | | rexr 10522 |
. . . . 5
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℝ*) |
68 | 67 | ad2antlr 723 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → 𝑏 ∈ ℝ*) |
69 | | pnfxr 10530 |
. . . . 5
⊢ +∞
∈ ℝ* |
70 | 69 | a1i 11 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → +∞ ∈
ℝ*) |
71 | 44 | simprd 496 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ∧ 𝑗 ∈ 𝐵 ∧ 𝑘 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝑏) |
72 | 71 | 3exp 1110 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (𝑗 ∈ 𝐵 → (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) |
73 | 32, 72 | ralrimi 3181 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ 𝑘 ∈ ℝ ∧ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)) |
74 | 73 | 3exp 1110 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (𝑘 ∈ ℝ → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)))) |
75 | 74 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (𝑘 ∈ ℝ → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)))) |
76 | 28, 75 | reximdai 3269 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) |
77 | 25, 76 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)) |
78 | 53 | breq1d 4966 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((𝐹‘𝑖) ≤ 𝑏 ↔ (𝐹‘𝑗) ≤ 𝑏)) |
79 | 52, 78 | imbi12d 346 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → ((ℎ ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑏) ↔ (ℎ ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) |
80 | 79 | cbvralv 3400 |
. . . . . . . 8
⊢
(∀𝑖 ∈
𝐵 (ℎ ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑏) ↔ ∀𝑗 ∈ 𝐵 (ℎ ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)) |
81 | 57 | imbi1d 343 |
. . . . . . . . 9
⊢ (ℎ = 𝑘 → ((ℎ ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏) ↔ (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) |
82 | 81 | ralbidv 3162 |
. . . . . . . 8
⊢ (ℎ = 𝑘 → (∀𝑗 ∈ 𝐵 (ℎ ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏) ↔ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) |
83 | 80, 82 | syl5bb 284 |
. . . . . . 7
⊢ (ℎ = 𝑘 → (∀𝑖 ∈ 𝐵 (ℎ ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑏) ↔ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏))) |
84 | 83 | cbvrexv 3401 |
. . . . . 6
⊢
(∃ℎ ∈
ℝ ∀𝑖 ∈
𝐵 (ℎ ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑏) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑏)) |
85 | 77, 84 | sylibr 235 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → ∃ℎ ∈ ℝ ∀𝑖 ∈ 𝐵 (ℎ ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑏)) |
86 | 18, 22, 68, 85 | limsupbnd1 14661 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (lim sup‘𝐹) ≤ 𝑏) |
87 | | ltpnf 12354 |
. . . . 5
⊢ (𝑏 ∈ ℝ → 𝑏 < +∞) |
88 | 87 | ad2antlr 723 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → 𝑏 < +∞) |
89 | 15, 68, 70, 86, 88 | xrlelttrd 12392 |
. . 3
⊢ (((𝜑 ∧ 𝑏 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) → (lim sup‘𝐹) < +∞) |
90 | 89, 65 | r19.29a 3249 |
. 2
⊢ (𝜑 → (lim sup‘𝐹) <
+∞) |
91 | | xrrebnd 12400 |
. . 3
⊢ ((lim
sup‘𝐹) ∈
ℝ* → ((lim sup‘𝐹) ∈ ℝ ↔ (-∞ < (lim
sup‘𝐹) ∧ (lim
sup‘𝐹) <
+∞))) |
92 | 14, 91 | syl 17 |
. 2
⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔
(-∞ < (lim sup‘𝐹) ∧ (lim sup‘𝐹) < +∞))) |
93 | 66, 90, 92 | mpbir2and 709 |
1
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ) |