Step | Hyp | Ref
| Expression |
1 | | liminfresico.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℝ) |
2 | 1 | rexrd 10426 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
3 | 2 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑀 ∈
ℝ*) |
4 | | pnfxr 10430 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
5 | 4 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → +∞ ∈
ℝ*) |
6 | | ressxr 10420 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
7 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → +∞ ∈
ℝ*) |
8 | | icossre 12566 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑀[,)+∞) ⊆
ℝ) |
9 | 1, 7, 8 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀[,)+∞) ⊆
ℝ) |
10 | 9 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀[,)+∞) ⊆
ℝ) |
11 | | liminfresico.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑍 = (𝑀[,)+∞) |
12 | 11 | eleq2i 2850 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (𝑀[,)+∞)) |
13 | 12 | biimpi 208 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ (𝑀[,)+∞)) |
14 | 13 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (𝑀[,)+∞)) |
15 | 10, 14 | sseldd 3821 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℝ) |
16 | 15 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑘 ∈ ℝ) |
17 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ (𝑘[,)+∞)) |
18 | | elicore 12538 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℝ ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ ℝ) |
19 | 16, 17, 18 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ ℝ) |
20 | 6, 19 | sseldi 3818 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ ℝ*) |
21 | 1 | ad2antrr 716 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑀 ∈ ℝ) |
22 | 2 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑀 ∈
ℝ*) |
23 | 4 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → +∞ ∈
ℝ*) |
24 | 22, 23, 14 | icogelbd 40675 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑀 ≤ 𝑘) |
25 | 24 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑀 ≤ 𝑘) |
26 | 6, 16 | sseldi 3818 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑘 ∈ ℝ*) |
27 | 26, 5, 17 | icogelbd 40675 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑘 ≤ 𝑦) |
28 | 21, 16, 19, 25, 27 | letrd 10533 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑀 ≤ 𝑦) |
29 | 19 | ltpnfd 12266 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 < +∞) |
30 | 3, 5, 20, 28, 29 | elicod 12536 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ (𝑀[,)+∞)) |
31 | 30, 11 | syl6eleqr 2869 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑘[,)+∞)) → 𝑦 ∈ 𝑍) |
32 | 31 | ssd 40165 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑘[,)+∞) ⊆ 𝑍) |
33 | | resima2 5681 |
. . . . . . . . 9
⊢ ((𝑘[,)+∞) ⊆ 𝑍 → ((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) = (𝐹 “ (𝑘[,)+∞))) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) = (𝐹 “ (𝑘[,)+∞))) |
35 | 34 | ineq1d 4035 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*) =
((𝐹 “ (𝑘[,)+∞)) ∩
ℝ*)) |
36 | 35 | infeq1d 8671 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → inf((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ) = inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
37 | 36 | mpteq2dva 4979 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ inf((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) = (𝑘 ∈ 𝑍 ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ))) |
38 | 37 | rneqd 5598 |
. . . 4
⊢ (𝜑 → ran (𝑘 ∈ 𝑍 ↦ inf((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) = ran (𝑘 ∈ 𝑍 ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ))) |
39 | 11, 9 | syl5eqss 3867 |
. . . . 5
⊢ (𝜑 → 𝑍 ⊆ ℝ) |
40 | 39 | mptima2 40352 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ ℝ ↦ inf((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍) = ran (𝑘 ∈ 𝑍 ↦ inf((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ))) |
41 | 39 | mptima2 40352 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍) = ran (𝑘 ∈ 𝑍 ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ))) |
42 | 38, 40, 41 | 3eqtr4d 2823 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ ℝ ↦ inf((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍) = ((𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍)) |
43 | 42 | supeq1d 8640 |
. 2
⊢ (𝜑 → sup(((𝑘 ∈ ℝ ↦ inf((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍), ℝ*, < ) = sup(((𝑘 ∈ ℝ ↦
inf(((𝐹 “ (𝑘[,)+∞)) ∩
ℝ*), ℝ*, < )) “ 𝑍), ℝ*, <
)) |
44 | | eqid 2777 |
. . 3
⊢ (𝑘 ∈ ℝ ↦
inf((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) = (𝑘 ∈ ℝ ↦ inf((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
45 | | liminfresico.3 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
46 | 45 | resexd 40230 |
. . 3
⊢ (𝜑 → (𝐹 ↾ 𝑍) ∈ V) |
47 | 11 | supeq1i 8641 |
. . . . 5
⊢ sup(𝑍, ℝ*, < ) =
sup((𝑀[,)+∞),
ℝ*, < ) |
48 | 47 | a1i 11 |
. . . 4
⊢ (𝜑 → sup(𝑍, ℝ*, < ) = sup((𝑀[,)+∞),
ℝ*, < )) |
49 | 1 | renepnfd 10427 |
. . . . 5
⊢ (𝜑 → 𝑀 ≠ +∞) |
50 | | icopnfsup 12983 |
. . . . 5
⊢ ((𝑀 ∈ ℝ*
∧ 𝑀 ≠ +∞)
→ sup((𝑀[,)+∞),
ℝ*, < ) = +∞) |
51 | 2, 49, 50 | syl2anc 579 |
. . . 4
⊢ (𝜑 → sup((𝑀[,)+∞), ℝ*, < ) =
+∞) |
52 | 48, 51 | eqtrd 2813 |
. . 3
⊢ (𝜑 → sup(𝑍, ℝ*, < ) =
+∞) |
53 | 44, 46, 39, 52 | liminfval2 40890 |
. 2
⊢ (𝜑 → (lim inf‘(𝐹 ↾ 𝑍)) = sup(((𝑘 ∈ ℝ ↦ inf((((𝐹 ↾ 𝑍) “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍), ℝ*, <
)) |
54 | | eqid 2777 |
. . 3
⊢ (𝑘 ∈ ℝ ↦
inf(((𝐹 “ (𝑘[,)+∞)) ∩
ℝ*), ℝ*, < )) = (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
55 | 54, 45, 39, 52 | liminfval2 40890 |
. 2
⊢ (𝜑 → (lim inf‘𝐹) = sup(((𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) “ 𝑍), ℝ*, <
)) |
56 | 43, 53, 55 | 3eqtr4d 2823 |
1
⊢ (𝜑 → (lim inf‘(𝐹 ↾ 𝑍)) = (lim inf‘𝐹)) |