Step | Hyp | Ref
| Expression |
1 | | limsuppnfdlem.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) |
2 | | reex 10833 |
. . . . . 6
⊢ ℝ
∈ V |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈
V) |
4 | | limsuppnfdlem.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
5 | 3, 4 | ssexd 5226 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ V) |
6 | 1, 5 | fexd 7052 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
7 | | limsuppnfdlem.g |
. . . 4
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
8 | 7 | limsupval 15048 |
. . 3
⊢ (𝐹 ∈ V → (lim
sup‘𝐹) = inf(ran
𝐺, ℝ*,
< )) |
9 | 6, 8 | syl 17 |
. 2
⊢ (𝜑 → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, <
)) |
10 | 1 | ffund 6558 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Fun 𝐹) |
11 | 10 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → Fun 𝐹) |
12 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ 𝐴) |
13 | 1 | fdmd 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → dom 𝐹 = 𝐴) |
14 | 13 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → dom 𝐹 = 𝐴) |
15 | 12, 14 | eleqtrrd 2842 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ dom 𝐹) |
16 | 11, 15 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹)) |
17 | 16 | ad4ant13 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → (Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹)) |
18 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → 𝑘 ∈ ℝ) |
19 | 18 | rexrd 10896 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → 𝑘 ∈ ℝ*) |
20 | | pnfxr 10900 |
. . . . . . . . . . . . . . . . 17
⊢ +∞
∈ ℝ* |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → +∞ ∈
ℝ*) |
22 | 4 | ssrexr 42660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
23 | 22 | sselda 3910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ ℝ*) |
24 | 23 | ad4ant13 751 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → 𝑗 ∈ ℝ*) |
25 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → 𝑘 ≤ 𝑗) |
26 | 4 | sselda 3910 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ ℝ) |
27 | 26 | ltpnfd 12726 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 < +∞) |
28 | 27 | ad4ant13 751 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → 𝑗 < +∞) |
29 | 19, 21, 24, 25, 28 | elicod 12998 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → 𝑗 ∈ (𝑘[,)+∞)) |
30 | | funfvima 7055 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐹 ∧ 𝑗 ∈ dom 𝐹) → (𝑗 ∈ (𝑘[,)+∞) → (𝐹‘𝑗) ∈ (𝐹 “ (𝑘[,)+∞)))) |
31 | 17, 29, 30 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → (𝐹‘𝑗) ∈ (𝐹 “ (𝑘[,)+∞))) |
32 | 1 | ffvelrnda 6913 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐹‘𝑗) ∈
ℝ*) |
33 | 32 | ad4ant13 751 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → (𝐹‘𝑗) ∈
ℝ*) |
34 | 31, 33 | elind 4117 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → (𝐹‘𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩
ℝ*)) |
35 | 34 | adantllr 719 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ≤ 𝑗) → (𝐹‘𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩
ℝ*)) |
36 | 35 | adantrr 717 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩
ℝ*)) |
37 | | simprr 773 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → 𝑥 ≤ (𝐹‘𝑗)) |
38 | | breq2 5066 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘𝑗) → (𝑥 ≤ 𝑦 ↔ 𝑥 ≤ (𝐹‘𝑗))) |
39 | 38 | rspcev 3544 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)
∧ 𝑥 ≤ (𝐹‘𝑗)) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥 ≤ 𝑦) |
40 | 36, 37, 39 | syl2anc 587 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥 ≤ 𝑦) |
41 | | limsuppnfdlem.u |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) |
42 | 41 | r19.21bi 3131 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) |
43 | 42 | r19.21bi 3131 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) → ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) |
44 | 43 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) |
45 | 40, 44 | r19.29a 3215 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥 ≤ 𝑦) |
46 | 45 | ralrimiva 3106 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → ∀𝑥 ∈ ℝ ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥 ≤ 𝑦) |
47 | | inss2 4153 |
. . . . . . . . 9
⊢ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)
⊆ ℝ* |
48 | | supxrunb3 42627 |
. . . . . . . . 9
⊢ (((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)
⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥 ≤ 𝑦 ↔ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ) = +∞)) |
49 | 47, 48 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (∀𝑥 ∈ ℝ ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥 ≤ 𝑦 ↔ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ) = +∞)) |
50 | 46, 49 | mpbid 235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ) = +∞) |
51 | 50 | mpteq2dva 5159 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) = (𝑘 ∈ ℝ ↦
+∞)) |
52 | 7, 51 | syl5eq 2791 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑘 ∈ ℝ ↦
+∞)) |
53 | 52 | rneqd 5816 |
. . . 4
⊢ (𝜑 → ran 𝐺 = ran (𝑘 ∈ ℝ ↦
+∞)) |
54 | | eqid 2738 |
. . . . 5
⊢ (𝑘 ∈ ℝ ↦
+∞) = (𝑘 ∈
ℝ ↦ +∞) |
55 | | ren0 42630 |
. . . . . 6
⊢ ℝ
≠ ∅ |
56 | 55 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ≠
∅) |
57 | 54, 56 | rnmptc 7031 |
. . . 4
⊢ (𝜑 → ran (𝑘 ∈ ℝ ↦ +∞) =
{+∞}) |
58 | 53, 57 | eqtrd 2778 |
. . 3
⊢ (𝜑 → ran 𝐺 = {+∞}) |
59 | 58 | infeq1d 9106 |
. 2
⊢ (𝜑 → inf(ran 𝐺, ℝ*, < ) =
inf({+∞}, ℝ*, < )) |
60 | | xrltso 12744 |
. . . 4
⊢ < Or
ℝ* |
61 | | infsn 9134 |
. . . 4
⊢ (( <
Or ℝ* ∧ +∞ ∈ ℝ*) →
inf({+∞}, ℝ*, < ) = +∞) |
62 | 60, 20, 61 | mp2an 692 |
. . 3
⊢
inf({+∞}, ℝ*, < ) = +∞ |
63 | 62 | a1i 11 |
. 2
⊢ (𝜑 → inf({+∞},
ℝ*, < ) = +∞) |
64 | 9, 59, 63 | 3eqtrd 2782 |
1
⊢ (𝜑 → (lim sup‘𝐹) = +∞) |