Step | Hyp | Ref
| Expression |
1 | | nfv 1922 |
. . . 4
⊢
Ⅎ𝑗𝜑 |
2 | | limsupgtlem.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | limsupgtlem.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 2, 3 | uzn0d 42646 |
. . . 4
⊢ (𝜑 → 𝑍 ≠ ∅) |
5 | | rnresss 5892 |
. . . . . . . 8
⊢ ran
(𝐹 ↾
(ℤ≥‘𝑗)) ⊆ ran 𝐹 |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ran (𝐹 ↾ (ℤ≥‘𝑗)) ⊆ ran 𝐹) |
7 | | limsupgtlem.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) |
8 | 7 | frexr 42605 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
9 | 8 | frnd 6558 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆
ℝ*) |
10 | 6, 9 | sstrd 3916 |
. . . . . 6
⊢ (𝜑 → ran (𝐹 ↾ (ℤ≥‘𝑗)) ⊆
ℝ*) |
11 | 10 | supxrcld 42338 |
. . . . 5
⊢ (𝜑 → sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
∈ ℝ*) |
12 | 11 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
∈ ℝ*) |
13 | | limsupgtlem.r |
. . . . . . 7
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ) |
14 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑘𝐹 |
15 | 14, 2, 3, 7 | limsupreuz 42961 |
. . . . . . 7
⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔
(∃𝑥 ∈ ℝ
∀𝑗 ∈ 𝑍 ∃𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘) ∧ ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥))) |
16 | 13, 15 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 ∃𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘) ∧ ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥)) |
17 | 16 | simpld 498 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 ∃𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)) |
18 | | rexr 10884 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
19 | 18 | ad4antlr 733 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 ≤ (𝐹‘𝑘)) → 𝑥 ∈ ℝ*) |
20 | 7 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐹:𝑍⟶ℝ) |
21 | 3 | uztrn2 12462 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
22 | 21 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
23 | 20, 22 | ffvelrnd 6910 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℝ) |
24 | 23 | rexrd 10888 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈
ℝ*) |
25 | 24 | 3impa 1112 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈
ℝ*) |
26 | 25 | ad5ant134 1369 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 ≤ (𝐹‘𝑘)) → (𝐹‘𝑘) ∈
ℝ*) |
27 | 11 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 ≤ (𝐹‘𝑘)) → sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
∈ ℝ*) |
28 | | simpr 488 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 ≤ (𝐹‘𝑘)) → 𝑥 ≤ (𝐹‘𝑘)) |
29 | 10 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ran (𝐹 ↾ (ℤ≥‘𝑗)) ⊆
ℝ*) |
30 | | fvres 6741 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
(ℤ≥‘𝑗) → ((𝐹 ↾ (ℤ≥‘𝑗))‘𝑘) = (𝐹‘𝑘)) |
31 | 30 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘𝑗) → (𝐹‘𝑘) = ((𝐹 ↾ (ℤ≥‘𝑗))‘𝑘)) |
32 | 31 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) = ((𝐹 ↾ (ℤ≥‘𝑗))‘𝑘)) |
33 | 7 | ffnd 6551 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 Fn 𝑍) |
34 | 33 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐹 Fn 𝑍) |
35 | 22 | ssd 42311 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (ℤ≥‘𝑗) ⊆ 𝑍) |
36 | | fnssres 6505 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn 𝑍 ∧ (ℤ≥‘𝑗) ⊆ 𝑍) → (𝐹 ↾ (ℤ≥‘𝑗)) Fn
(ℤ≥‘𝑗)) |
37 | 34, 35, 36 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹 ↾ (ℤ≥‘𝑗)) Fn
(ℤ≥‘𝑗)) |
38 | 37 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹 ↾ (ℤ≥‘𝑗)) Fn
(ℤ≥‘𝑗)) |
39 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ (ℤ≥‘𝑗)) |
40 | 38, 39 | fnfvelrnd 42488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹 ↾ (ℤ≥‘𝑗))‘𝑘) ∈ ran (𝐹 ↾ (ℤ≥‘𝑗))) |
41 | 32, 40 | eqeltrd 2838 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ran (𝐹 ↾ (ℤ≥‘𝑗))) |
42 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ sup(ran
(𝐹 ↾
(ℤ≥‘𝑗)), ℝ*, < ) = sup(ran
(𝐹 ↾
(ℤ≥‘𝑗)), ℝ*, <
) |
43 | 29, 41, 42 | supxrubd 42344 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ≤ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
)) |
44 | 43 | 3impa 1112 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ≤ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
)) |
45 | 44 | ad5ant134 1369 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 ≤ (𝐹‘𝑘)) → (𝐹‘𝑘) ≤ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
)) |
46 | 19, 26, 27, 28, 45 | xrletrd 12757 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 ≤ (𝐹‘𝑘)) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
)) |
47 | 46 | rexlimdva2 3211 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) → (∃𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
))) |
48 | 47 | ralimdva 3100 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑗 ∈ 𝑍 ∃𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘) → ∀𝑗 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
))) |
49 | 48 | reximdva 3198 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 ∃𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
))) |
50 | 17, 49 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
)) |
51 | | limsupgtlem.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
52 | 51 | rphalfcld 12645 |
. . . 4
⊢ (𝜑 → (𝑋 / 2) ∈
ℝ+) |
53 | 1, 4, 12, 50, 52 | infrpgernmpt 42688 |
. . 3
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ (inf(ran (𝑗 ∈
𝑍 ↦ sup(ran (𝐹 ↾
(ℤ≥‘𝑗)), ℝ*, < )),
ℝ*, < ) +𝑒 (𝑋 / 2))) |
54 | | simp3 1140 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ (inf(ran (𝑗 ∈
𝑍 ↦ sup(ran (𝐹 ↾
(ℤ≥‘𝑗)), ℝ*, < )),
ℝ*, < ) +𝑒 (𝑋 / 2))) → sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ (inf(ran (𝑗 ∈
𝑍 ↦ sup(ran (𝐹 ↾
(ℤ≥‘𝑗)), ℝ*, < )),
ℝ*, < ) +𝑒 (𝑋 / 2))) |
55 | 2, 3, 8 | limsupvaluz 42932 |
. . . . . . . . . 10
⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑗 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
)), ℝ*, < )) |
56 | 55 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → inf(ran (𝑗 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
)), ℝ*, < ) = (lim sup‘𝐹)) |
57 | 56 | oveq1d 7233 |
. . . . . . . 8
⊢ (𝜑 → (inf(ran (𝑗 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
)), ℝ*, < ) +𝑒 (𝑋 / 2)) = ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) |
58 | 57 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ (inf(ran (𝑗 ∈
𝑍 ↦ sup(ran (𝐹 ↾
(ℤ≥‘𝑗)), ℝ*, < )),
ℝ*, < ) +𝑒 (𝑋 / 2))) → (inf(ran (𝑗 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
)), ℝ*, < ) +𝑒 (𝑋 / 2)) = ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) |
59 | 54, 58 | breqtrd 5084 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ (inf(ran (𝑗 ∈
𝑍 ↦ sup(ran (𝐹 ↾
(ℤ≥‘𝑗)), ℝ*, < )),
ℝ*, < ) +𝑒 (𝑋 / 2))) → sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) |
60 | 24 | 3adantl3 1170 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈
ℝ*) |
61 | | simpl1 1193 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝜑) |
62 | 61, 11 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
∈ ℝ*) |
63 | 3 | fvexi 6736 |
. . . . . . . . . . . . . . 15
⊢ 𝑍 ∈ V |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ∈ V) |
65 | 7, 64 | fexd 7048 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ V) |
66 | 65 | limsupcld 42914 |
. . . . . . . . . . . 12
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ*) |
67 | 51 | rpred 12633 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ ℝ) |
68 | 67 | rehalfcld 12082 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 / 2) ∈ ℝ) |
69 | 68 | rexrd 10888 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 / 2) ∈
ℝ*) |
70 | 66, 69 | xaddcld 12896 |
. . . . . . . . . . 11
⊢ (𝜑 → ((lim sup‘𝐹) +𝑒 (𝑋 / 2)) ∈
ℝ*) |
71 | 61, 70 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → ((lim sup‘𝐹) +𝑒 (𝑋 / 2)) ∈
ℝ*) |
72 | 43 | 3adantl3 1170 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (𝐹‘𝑘) ≤ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, <
)) |
73 | | simpl3 1195 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) |
74 | 60, 62, 71, 72, 73 | xrletrd 12757 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (𝐹‘𝑘) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) |
75 | 13, 68 | rexaddd 12829 |
. . . . . . . . . 10
⊢ (𝜑 → ((lim sup‘𝐹) +𝑒 (𝑋 / 2)) = ((lim sup‘𝐹) + (𝑋 / 2))) |
76 | 61, 75 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → ((lim sup‘𝐹) +𝑒 (𝑋 / 2)) = ((lim sup‘𝐹) + (𝑋 / 2))) |
77 | 74, 76 | breqtrd 5084 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (𝐹‘𝑘) ≤ ((lim sup‘𝐹) + (𝑋 / 2))) |
78 | 68 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝑋 / 2) ∈ ℝ) |
79 | 13 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (lim sup‘𝐹) ∈
ℝ) |
80 | 23, 78, 79 | lesubaddd 11434 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) ↔ (𝐹‘𝑘) ≤ ((lim sup‘𝐹) + (𝑋 / 2)))) |
81 | 80 | 3adantl3 1170 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) ↔ (𝐹‘𝑘) ≤ ((lim sup‘𝐹) + (𝑋 / 2)))) |
82 | 77, 81 | mpbird 260 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → ((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) |
83 | 82 | ralrimiva 3105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ ((lim sup‘𝐹)
+𝑒 (𝑋 /
2))) → ∀𝑘
∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) |
84 | 59, 83 | syld3an3 1411 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ (inf(ran (𝑗 ∈
𝑍 ↦ sup(ran (𝐹 ↾
(ℤ≥‘𝑗)), ℝ*, < )),
ℝ*, < ) +𝑒 (𝑋 / 2))) → ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) |
85 | 84 | 3exp 1121 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝑍 → (sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ (inf(ran (𝑗 ∈
𝑍 ↦ sup(ran (𝐹 ↾
(ℤ≥‘𝑗)), ℝ*, < )),
ℝ*, < ) +𝑒 (𝑋 / 2)) → ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)))) |
86 | 1, 85 | reximdai 3235 |
. . 3
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 sup(ran (𝐹 ↾ (ℤ≥‘𝑗)), ℝ*, < )
≤ (inf(ran (𝑗 ∈
𝑍 ↦ sup(ran (𝐹 ↾
(ℤ≥‘𝑗)), ℝ*, < )),
ℝ*, < ) +𝑒 (𝑋 / 2)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹))) |
87 | 53, 86 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) |
88 | | simpll 767 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝜑) |
89 | 7 | ffvelrnda 6909 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
90 | 67 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑋 ∈ ℝ) |
91 | 89, 90 | resubcld 11265 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) − 𝑋) ∈ ℝ) |
92 | 91 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → ((𝐹‘𝑘) − 𝑋) ∈ ℝ) |
93 | 68 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑋 / 2) ∈ ℝ) |
94 | 89, 93 | resubcld 11265 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) − (𝑋 / 2)) ∈ ℝ) |
95 | 94 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → ((𝐹‘𝑘) − (𝑋 / 2)) ∈ ℝ) |
96 | 13 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → (lim sup‘𝐹) ∈ ℝ) |
97 | 51 | rphalfltd 42678 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 / 2) < 𝑋) |
98 | 97 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑋 / 2) < 𝑋) |
99 | 93, 90, 89, 98 | ltsub2dd 11450 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) − 𝑋) < ((𝐹‘𝑘) − (𝑋 / 2))) |
100 | 99 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → ((𝐹‘𝑘) − 𝑋) < ((𝐹‘𝑘) − (𝑋 / 2))) |
101 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → ((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) |
102 | 92, 95, 96, 100, 101 | ltletrd 10997 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → ((𝐹‘𝑘) − 𝑋) < (lim sup‘𝐹)) |
103 | 102 | ex 416 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) → ((𝐹‘𝑘) − 𝑋) < (lim sup‘𝐹))) |
104 | 88, 22, 103 | syl2anc 587 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) → ((𝐹‘𝑘) − 𝑋) < (lim sup‘𝐹))) |
105 | 104 | ralimdva 3100 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) → ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − 𝑋) < (lim sup‘𝐹))) |
106 | 105 | reximdva 3198 |
. 2
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − 𝑋) < (lim sup‘𝐹))) |
107 | 87, 106 | mpd 15 |
1
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − 𝑋) < (lim sup‘𝐹)) |