| Step | Hyp | Ref
| Expression |
| 1 | | limsupresico.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 2 | 1 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
| 3 | 2 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑀 ∈
ℝ*) |
| 4 | | pnfxr 11315 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
| 5 | 4 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → +∞ ∈
ℝ*) |
| 6 | | ressxr 11305 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
| 7 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 8 | | icossre 13468 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑀[,)+∞) ⊆
ℝ) |
| 9 | 1, 7, 8 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀[,)+∞) ⊆
ℝ) |
| 10 | 9 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀[,)+∞) ⊆
ℝ) |
| 11 | | limsupresico.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑍 = (𝑀[,)+∞) |
| 12 | 11 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (𝑀[,)+∞)) |
| 13 | 12 | biimpi 216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ (𝑀[,)+∞)) |
| 14 | 13 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (𝑀[,)+∞)) |
| 15 | 10, 14 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℝ) |
| 16 | 15 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑘 ∈ ℝ) |
| 17 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ (𝑘[,)+∞)) |
| 18 | | elicore 13439 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℝ ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ ℝ) |
| 19 | 16, 17, 18 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ ℝ) |
| 20 | 6, 19 | sselid 3981 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ ℝ*) |
| 21 | 1 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑀 ∈ ℝ) |
| 22 | 2 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑀 ∈
ℝ*) |
| 23 | 4 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → +∞ ∈
ℝ*) |
| 24 | 22, 23, 14 | icogelbd 45571 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑀 ≤ 𝑘) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑀 ≤ 𝑘) |
| 26 | 6, 16 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑘 ∈ ℝ*) |
| 27 | 26, 5, 17 | icogelbd 45571 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑘 ≤ 𝑦) |
| 28 | 21, 16, 19, 25, 27 | letrd 11418 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑀 ≤ 𝑦) |
| 29 | 19 | ltpnfd 13163 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 < +∞) |
| 30 | 3, 5, 20, 28, 29 | elicod 13437 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ (𝑀[,)+∞)) |
| 31 | 30, 11 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ 𝑍) |
| 32 | 31 | ssd 45085 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑘[,)+∞) ⊆ 𝑍) |
| 33 | | resima2 6034 |
. . . . . . . . 9
⊢ ((𝑘[,)+∞) ⊆ 𝑍 → ((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) = (𝐹 “ (𝑘[,)+∞))) |
| 34 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) = (𝐹 “ (𝑘[,)+∞))) |
| 35 | 34 | ineq1d 4219 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*) =
((𝐹 “ (𝑘[,)+∞)) ∩
ℝ*)) |
| 36 | 35 | supeq1d 9486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → sup((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ) = sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 37 | 36 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ sup((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) = (𝑘 ∈ 𝑍 ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ))) |
| 38 | 37 | rneqd 5949 |
. . . 4
⊢ (𝜑 → ran (𝑘 ∈ 𝑍 ↦ sup((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) = ran (𝑘 ∈ 𝑍 ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ))) |
| 39 | 11, 9 | eqsstrid 4022 |
. . . . 5
⊢ (𝜑 → 𝑍 ⊆ ℝ) |
| 40 | 39 | mptimass 6091 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ ℝ ↦ sup((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍) = ran (𝑘 ∈ 𝑍 ↦ sup((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ))) |
| 41 | 39 | mptimass 6091 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍) = ran (𝑘 ∈ 𝑍 ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ))) |
| 42 | 38, 40, 41 | 3eqtr4d 2787 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ ℝ ↦ sup((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍) = ((𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍)) |
| 43 | 42 | infeq1d 9517 |
. 2
⊢ (𝜑 → inf(((𝑘 ∈ ℝ ↦ sup((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍), ℝ*, < ) = inf(((𝑘 ∈ ℝ ↦
sup(((𝐹 “ (𝑘[,)+∞)) ∩
ℝ*), ℝ*, < )) “ 𝑍), ℝ*, <
)) |
| 44 | | eqid 2737 |
. . 3
⊢ (𝑘 ∈ ℝ ↦
sup((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) = (𝑘 ∈ ℝ ↦ sup((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 45 | | limsupresico.3 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
| 46 | 45 | resexd 6046 |
. . 3
⊢ (𝜑 → (𝐹 ↾ 𝑍) ∈ V) |
| 47 | 11 | supeq1i 9487 |
. . . . 5
⊢ sup(𝑍, ℝ*, < ) =
sup((𝑀[,)+∞),
ℝ*, < ) |
| 48 | 47 | a1i 11 |
. . . 4
⊢ (𝜑 → sup(𝑍, ℝ*, < ) = sup((𝑀[,)+∞),
ℝ*, < )) |
| 49 | 1 | renepnfd 11312 |
. . . . 5
⊢ (𝜑 → 𝑀 ≠ +∞) |
| 50 | | icopnfsup 13905 |
. . . . 5
⊢ ((𝑀 ∈ ℝ*
∧ 𝑀 ≠ +∞)
→ sup((𝑀[,)+∞),
ℝ*, < ) = +∞) |
| 51 | 2, 49, 50 | syl2anc 584 |
. . . 4
⊢ (𝜑 → sup((𝑀[,)+∞), ℝ*, < ) =
+∞) |
| 52 | 48, 51 | eqtrd 2777 |
. . 3
⊢ (𝜑 → sup(𝑍, ℝ*, < ) =
+∞) |
| 53 | 44, 46, 39, 52 | limsupval2 15516 |
. 2
⊢ (𝜑 → (lim sup‘(𝐹 ↾ 𝑍)) = inf(((𝑘 ∈ ℝ ↦ sup((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍), ℝ*, <
)) |
| 54 | | eqid 2737 |
. . 3
⊢ (𝑘 ∈ ℝ ↦
sup(((𝐹 “ (𝑘[,)+∞)) ∩
ℝ*), ℝ*, < )) = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 55 | 54, 45, 39, 52 | limsupval2 15516 |
. 2
⊢ (𝜑 → (lim sup‘𝐹) = inf(((𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍), ℝ*, <
)) |
| 56 | 43, 53, 55 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (lim sup‘(𝐹 ↾ 𝑍)) = (lim sup‘𝐹)) |