Step | Hyp | Ref
| Expression |
1 | | nfv 1892 |
. . . 4
⊢
Ⅎ𝑚𝜑 |
2 | | smflimsuplem4.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | smflimsuplem4.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | | smflimsuplem4.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
5 | 3, 4 | eluzelz2d 41248 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
6 | | eqid 2795 |
. . . 4
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
7 | | fvexd 6553 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
8 | | fvexd 6553 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
9 | 1, 2, 5, 3, 6, 7, 8 | limsupequzmpt 41571 |
. . 3
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ (ℤ≥‘𝑁) ↦ ((𝐹‘𝑚)‘𝑥)))) |
10 | | smflimsuplem4.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ SAlg) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑆 ∈ SAlg) |
12 | 3, 4 | uzssd2 41252 |
. . . . . . . . 9
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆ 𝑍) |
13 | 12 | sselda 3889 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑚 ∈ 𝑍) |
14 | | smflimsuplem4.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
15 | 14 | ffvelrnda 6716 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
16 | 13, 15 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
17 | | eqid 2795 |
. . . . . . 7
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
18 | 11, 16, 17 | smff 42571 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
19 | | smflimsuplem4.e |
. . . . . . . 8
⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
20 | | smflimsuplem4.h |
. . . . . . . 8
⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
21 | 3, 19, 20, 13 | smflimsuplem1 42656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → dom (𝐻‘𝑚) ⊆ dom (𝐹‘𝑚)) |
22 | | smflimsuplem4.i |
. . . . . . . . 9
⊢ (𝜑 → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)dom (𝐻‘𝑛)) |
23 | 22 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)dom (𝐻‘𝑛)) |
24 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑚 ∈ (ℤ≥‘𝑁)) |
25 | | fveq2 6538 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝐻‘𝑛) = (𝐻‘𝑚)) |
26 | 25 | dmeqd 5660 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → dom (𝐻‘𝑛) = dom (𝐻‘𝑚)) |
27 | 26 | eleq2d 2868 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑥 ∈ dom (𝐻‘𝑛) ↔ 𝑥 ∈ dom (𝐻‘𝑚))) |
28 | 23, 24, 27 | eliind 40891 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ dom (𝐻‘𝑚)) |
29 | 21, 28 | sseldd 3890 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
30 | 18, 29 | ffvelrnd 6717 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
31 | 30 | rexrd 10537 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑚)‘𝑥) ∈
ℝ*) |
32 | 1, 5, 6, 31 | limsupvaluzmpt 41559 |
. . 3
⊢ (𝜑 → (lim sup‘(𝑚 ∈
(ℤ≥‘𝑁) ↦ ((𝐹‘𝑚)‘𝑥))) = inf(ran (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
33 | 9, 32 | eqtrd 2831 |
. 2
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = inf(ran (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
34 | | smflimsuplem4.1 |
. . 3
⊢
Ⅎ𝑛𝜑 |
35 | 12 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) →
(ℤ≥‘𝑁) ⊆ 𝑍) |
36 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ (ℤ≥‘𝑁)) |
37 | 35, 36 | sseldd 3890 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ 𝑍) |
38 | 20 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)))) |
39 | | fvex 6551 |
. . . . . . . . . . . . . . 15
⊢ (𝐸‘𝑛) ∈ V |
40 | 39 | mptex 6852 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈
V |
41 | 40 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈
V) |
42 | 38, 41 | fvmpt2d 6647 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
43 | 37, 42 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
44 | 43 | dmeqd 5660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝐻‘𝑛) = dom (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
45 | | xrltso 12384 |
. . . . . . . . . . . . 13
⊢ < Or
ℝ* |
46 | 45 | supex 8773 |
. . . . . . . . . . . 12
⊢ sup(ran
(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
V |
47 | | eqid 2795 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
48 | 46, 47 | dmmpti 6360 |
. . . . . . . . . . 11
⊢ dom
(𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝐸‘𝑛) |
49 | 48 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝐸‘𝑛)) |
50 | 44, 49 | eqtrd 2831 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝐻‘𝑛) = (𝐸‘𝑛)) |
51 | 34, 50 | iineq2d 4847 |
. . . . . . . 8
⊢ (𝜑 → ∩ 𝑛 ∈ (ℤ≥‘𝑁)dom (𝐻‘𝑛) = ∩ 𝑛 ∈
(ℤ≥‘𝑁)(𝐸‘𝑛)) |
52 | 22, 51 | eleqtrd 2885 |
. . . . . . 7
⊢ (𝜑 → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)(𝐸‘𝑛)) |
53 | 52 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)(𝐸‘𝑛)) |
54 | | eliinid 40936 |
. . . . . 6
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ (ℤ≥‘𝑁)(𝐸‘𝑛) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ (𝐸‘𝑛)) |
55 | 53, 36, 54 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ (𝐸‘𝑛)) |
56 | 46 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑥 ∈ (𝐸‘𝑛)) → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
V) |
57 | 43, 56 | fvmpt2d 6647 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑥 ∈ (𝐸‘𝑛)) → ((𝐻‘𝑛)‘𝑥) = sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
58 | 55, 57 | mpdan 683 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) = sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
59 | | eqid 2795 |
. . . . . . . . . 10
⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} = {𝑥 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} |
60 | 3 | eluzelz2 41236 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
61 | | eqid 2795 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
62 | 60, 61 | uzn0d 41260 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ≠ ∅) |
63 | | fvex 6551 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑚) ∈ V |
64 | 63 | dmex 7472 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐹‘𝑚) ∈ V |
65 | 64 | rgenw 3117 |
. . . . . . . . . . . . 13
⊢
∀𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V |
66 | 65 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
67 | 62, 66 | iinexd 40958 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
68 | 67 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
69 | 59, 68 | rabexd 5127 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) |
70 | 37, 69 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) |
71 | 19 | fvmpt2 6645 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ∧ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) → (𝐸‘𝑛) = {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
72 | 37, 70, 71 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐸‘𝑛) = {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
73 | 55, 72 | eleqtrd 2885 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
74 | | rabid 3337 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ↔ (𝑥 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ)) |
75 | 73, 74 | sylib 219 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ)) |
76 | 75 | simprd 496 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ) |
77 | 58, 76 | eqeltrd 2883 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) ∈ ℝ) |
78 | 34, 58 | mpteq2da 5054 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) = (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
79 | | nfv 1892 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
80 | | fveq2 6538 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑘)) |
81 | 80 | mpteq1d 5049 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥))) |
82 | 81 | rneqd 5690 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥))) |
83 | 82 | supeq1d 8756 |
. . . . 5
⊢ (𝑛 = 𝑘 → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) = sup(ran
(𝑚 ∈
(ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
84 | | nfv 1892 |
. . . . . . . 8
⊢
Ⅎ𝑚(𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) |
85 | | eluzelz 12103 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → 𝑛 ∈ ℤ) |
86 | 85 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 ∈ ℤ) |
87 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 = (𝑛 + 1)) |
88 | 86 | peano2zd 11939 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → (𝑛 + 1) ∈ ℤ) |
89 | 87, 88 | eqeltrd 2883 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 ∈ ℤ) |
90 | 86 | zred 11936 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 ∈ ℝ) |
91 | 89 | zred 11936 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 ∈ ℝ) |
92 | 90 | ltp1d 11418 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 < (𝑛 + 1)) |
93 | 87 | eqcomd 2801 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → (𝑛 + 1) = 𝑘) |
94 | 92, 93 | breqtrd 4988 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 < 𝑘) |
95 | 90, 91, 94 | ltled 10635 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 ≤ 𝑘) |
96 | 61, 86, 89, 95 | eluzd 41243 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 ∈ (ℤ≥‘𝑛)) |
97 | | uzss 12114 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → (ℤ≥‘𝑘) ⊆
(ℤ≥‘𝑛)) |
98 | 96, 97 | syl 17 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) →
(ℤ≥‘𝑘) ⊆ (ℤ≥‘𝑛)) |
99 | | fvexd 6553 |
. . . . . . . 8
⊢ (((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
100 | 84, 98, 99 | rnmptss2 41089 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) |
101 | 100 | 3adant1 1123 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) |
102 | | nfv 1892 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) |
103 | | eqid 2795 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) |
104 | | simpll 763 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
105 | 37, 104 | syldanl 601 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
106 | 6 | uztrn2 12111 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑁)) |
107 | 106 | adantll 710 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑁)) |
108 | 105, 107,
30 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
109 | 102, 103,
108 | rnmptssd 41017 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ℝ) |
110 | | ressxr 10531 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
111 | 110 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ℝ ⊆
ℝ*) |
112 | 109, 111 | sstrd 3899 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆
ℝ*) |
113 | 112 | 3adant3 1125 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆
ℝ*) |
114 | | supxrss 12575 |
. . . . . 6
⊢ ((ran
(𝑚 ∈
(ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ∧ ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ℝ*) →
sup(ran (𝑚 ∈
(ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ≤ sup(ran
(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
115 | 101, 113,
114 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ≤ sup(ran
(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
116 | | smflimsuplem4.c |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ ) |
117 | 3 | fvexi 6552 |
. . . . . . . . 9
⊢ 𝑍 ∈ V |
118 | 117 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ V) |
119 | | fvexd 6553 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛)‘𝑥) ∈ V) |
120 | | fvexd 6553 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘𝑁) ∈ V) |
121 | 34, 36 | ssdf 40897 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑁)) |
122 | | fvexd 6553 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) ∈ V) |
123 | | eqidd 2796 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) = ((𝐻‘𝑛)‘𝑥)) |
124 | 34, 5, 6, 118, 12, 119, 120, 121, 122, 123 | climeldmeqmpt 41510 |
. . . . . . 7
⊢ (𝜑 → ((𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ ↔ (𝑛 ∈
(ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ )) |
125 | 116, 124 | mpbid 233 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ ) |
126 | 78, 125 | eqeltrrd 2884 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈ dom
⇝ ) |
127 | 34, 79, 5, 6, 76, 83, 115, 126 | climinf2mpt 41556 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ⇝
inf(ran (𝑛 ∈
(ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
128 | 78, 127 | eqbrtrd 4984 |
. . 3
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) ⇝ inf(ran (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
129 | 34, 5, 6, 77, 128 | climreclmpt 41526 |
. 2
⊢ (𝜑 → inf(ran (𝑛 ∈
(ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < ) ∈ ℝ) |
130 | 33, 129 | eqeltrd 2883 |
1
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) |