Step | Hyp | Ref
| Expression |
1 | | nfv 1917 |
. . . 4
⊢
Ⅎ𝑚𝜑 |
2 | | smflimsuplem4.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | smflimsuplem4.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | | smflimsuplem4.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
5 | 3, 4 | eluzelz2d 43584 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
6 | | eqid 2736 |
. . . 4
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
7 | | fvexd 6854 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
8 | | fvexd 6854 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
9 | 1, 2, 5, 3, 6, 7, 8 | limsupequzmpt 43902 |
. . 3
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ (ℤ≥‘𝑁) ↦ ((𝐹‘𝑚)‘𝑥)))) |
10 | | smflimsuplem4.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ SAlg) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑆 ∈ SAlg) |
12 | 3, 4 | uzssd2 43588 |
. . . . . . . . 9
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆ 𝑍) |
13 | 12 | sselda 3942 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑚 ∈ 𝑍) |
14 | | smflimsuplem4.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
15 | 14 | ffvelcdmda 7031 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
16 | 13, 15 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
17 | | eqid 2736 |
. . . . . . 7
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
18 | 11, 16, 17 | smff 44905 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
19 | | smflimsuplem4.e |
. . . . . . . 8
⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
20 | | smflimsuplem4.h |
. . . . . . . 8
⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
21 | 3, 19, 20, 13 | smflimsuplem1 44993 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → dom (𝐻‘𝑚) ⊆ dom (𝐹‘𝑚)) |
22 | | smflimsuplem4.i |
. . . . . . . . 9
⊢ (𝜑 → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)dom (𝐻‘𝑛)) |
23 | 22 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)dom (𝐻‘𝑛)) |
24 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑚 ∈ (ℤ≥‘𝑁)) |
25 | | fveq2 6839 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝐻‘𝑛) = (𝐻‘𝑚)) |
26 | 25 | dmeqd 5859 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → dom (𝐻‘𝑛) = dom (𝐻‘𝑚)) |
27 | 26 | eleq2d 2823 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑥 ∈ dom (𝐻‘𝑛) ↔ 𝑥 ∈ dom (𝐻‘𝑚))) |
28 | 23, 24, 27 | eliind 43221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ dom (𝐻‘𝑚)) |
29 | 21, 28 | sseldd 3943 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
30 | 18, 29 | ffvelcdmd 7032 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
31 | 30 | rexrd 11201 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑚)‘𝑥) ∈
ℝ*) |
32 | 1, 5, 6, 31 | limsupvaluzmpt 43890 |
. . 3
⊢ (𝜑 → (lim sup‘(𝑚 ∈
(ℤ≥‘𝑁) ↦ ((𝐹‘𝑚)‘𝑥))) = inf(ran (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
33 | 9, 32 | eqtrd 2776 |
. 2
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = inf(ran (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
34 | | smflimsuplem4.1 |
. . 3
⊢
Ⅎ𝑛𝜑 |
35 | 12 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) →
(ℤ≥‘𝑁) ⊆ 𝑍) |
36 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ (ℤ≥‘𝑁)) |
37 | 35, 36 | sseldd 3943 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ 𝑍) |
38 | 20 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)))) |
39 | | fvex 6852 |
. . . . . . . . . . . . . . 15
⊢ (𝐸‘𝑛) ∈ V |
40 | 39 | mptex 7169 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈
V |
41 | 40 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈
V) |
42 | 38, 41 | fvmpt2d 6958 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
43 | 37, 42 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
44 | 43 | dmeqd 5859 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝐻‘𝑛) = dom (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
45 | | xrltso 13052 |
. . . . . . . . . . . . 13
⊢ < Or
ℝ* |
46 | 45 | supex 9395 |
. . . . . . . . . . . 12
⊢ sup(ran
(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
V |
47 | | eqid 2736 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
48 | 46, 47 | dmmpti 6642 |
. . . . . . . . . . 11
⊢ dom
(𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝐸‘𝑛) |
49 | 48 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝐸‘𝑛)) |
50 | 44, 49 | eqtrd 2776 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝐻‘𝑛) = (𝐸‘𝑛)) |
51 | 34, 50 | iineq2d 4975 |
. . . . . . . 8
⊢ (𝜑 → ∩ 𝑛 ∈ (ℤ≥‘𝑁)dom (𝐻‘𝑛) = ∩ 𝑛 ∈
(ℤ≥‘𝑁)(𝐸‘𝑛)) |
52 | 22, 51 | eleqtrd 2840 |
. . . . . . 7
⊢ (𝜑 → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)(𝐸‘𝑛)) |
53 | 52 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)(𝐸‘𝑛)) |
54 | | eliinid 43263 |
. . . . . 6
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ (ℤ≥‘𝑁)(𝐸‘𝑛) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ (𝐸‘𝑛)) |
55 | 53, 36, 54 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ (𝐸‘𝑛)) |
56 | 46 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑥 ∈ (𝐸‘𝑛)) → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
V) |
57 | 43, 56 | fvmpt2d 6958 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑥 ∈ (𝐸‘𝑛)) → ((𝐻‘𝑛)‘𝑥) = sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
58 | 55, 57 | mpdan 685 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) = sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
59 | | eqid 2736 |
. . . . . . . . . 10
⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} = {𝑥 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} |
60 | 3 | eluzelz2 43574 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
61 | | eqid 2736 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
62 | 60, 61 | uzn0d 43596 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ≠ ∅) |
63 | | fvex 6852 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑚) ∈ V |
64 | 63 | dmex 7844 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐹‘𝑚) ∈ V |
65 | 64 | rgenw 3066 |
. . . . . . . . . . . . 13
⊢
∀𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V |
66 | 65 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
67 | 62, 66 | iinexd 43285 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
68 | 67 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
69 | 59, 68 | rabexd 5288 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) |
70 | 37, 69 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) |
71 | 19 | fvmpt2 6956 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ∧ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) → (𝐸‘𝑛) = {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
72 | 37, 70, 71 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐸‘𝑛) = {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
73 | 55, 72 | eleqtrd 2840 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
74 | | rabid 3425 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ↔ (𝑥 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ)) |
75 | 73, 74 | sylib 217 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ)) |
76 | 75 | simprd 496 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ) |
77 | 58, 76 | eqeltrd 2838 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) ∈ ℝ) |
78 | 34, 58 | mpteq2da 5201 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) = (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
79 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
80 | | fveq2 6839 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑘)) |
81 | 80 | mpteq1d 5198 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥))) |
82 | 81 | rneqd 5891 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥))) |
83 | 82 | supeq1d 9378 |
. . . . 5
⊢ (𝑛 = 𝑘 → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) = sup(ran
(𝑚 ∈
(ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
84 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑚(𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) |
85 | | eluzelz 12769 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → 𝑛 ∈ ℤ) |
86 | 85 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 ∈ ℤ) |
87 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 = (𝑛 + 1)) |
88 | 86 | peano2zd 12606 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → (𝑛 + 1) ∈ ℤ) |
89 | 87, 88 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 ∈ ℤ) |
90 | 86 | zred 12603 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 ∈ ℝ) |
91 | 89 | zred 12603 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 ∈ ℝ) |
92 | 90 | ltp1d 12081 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 < (𝑛 + 1)) |
93 | 87 | eqcomd 2742 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → (𝑛 + 1) = 𝑘) |
94 | 92, 93 | breqtrd 5129 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 < 𝑘) |
95 | 90, 91, 94 | ltled 11299 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 ≤ 𝑘) |
96 | 61, 86, 89, 95 | eluzd 43580 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 ∈ (ℤ≥‘𝑛)) |
97 | | uzss 12782 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → (ℤ≥‘𝑘) ⊆
(ℤ≥‘𝑛)) |
98 | 96, 97 | syl 17 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) →
(ℤ≥‘𝑘) ⊆ (ℤ≥‘𝑛)) |
99 | | fvexd 6854 |
. . . . . . . 8
⊢ (((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
100 | 84, 98, 99 | rnmptss2 43421 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) |
101 | 100 | 3adant1 1130 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) |
102 | | nfv 1917 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) |
103 | | eqid 2736 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) |
104 | | simpll 765 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
105 | 37, 104 | syldanl 602 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
106 | 6 | uztrn2 12778 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑁)) |
107 | 106 | adantll 712 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑁)) |
108 | 105, 107,
30 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
109 | 102, 103,
108 | rnmptssd 43352 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ℝ) |
110 | | ressxr 11195 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
111 | 110 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ℝ ⊆
ℝ*) |
112 | 109, 111 | sstrd 3952 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆
ℝ*) |
113 | 112 | 3adant3 1132 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆
ℝ*) |
114 | | supxrss 13243 |
. . . . . 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 6853 |
. . . . . . . . 9
⊢ 𝑍 ∈ V |
118 | 117 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ V) |
119 | | fvexd 6854 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛)‘𝑥) ∈ V) |
120 | | fvexd 6854 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘𝑁) ∈ V) |
121 | 34, 36 | ssdf 43227 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑁)) |
122 | | fvexd 6854 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) ∈ V) |
123 | | eqidd 2737 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) = ((𝐻‘𝑛)‘𝑥)) |
124 | 34, 5, 6, 118, 12, 119, 120, 121, 122, 123 | climeldmeqmpt 43841 |
. . . . . . 7
⊢ (𝜑 → ((𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ ↔ (𝑛 ∈
(ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ )) |
125 | 116, 124 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ ) |
126 | 78, 125 | eqeltrrd 2839 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈ dom
⇝ ) |
127 | 34, 79, 5, 6, 76, 83, 115, 126 | climinf2mpt 43887 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ⇝
inf(ran (𝑛 ∈
(ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
128 | 78, 127 | eqbrtrd 5125 |
. . 3
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) ⇝ inf(ran (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
129 | 34, 5, 6, 77, 128 | climreclmpt 43857 |
. 2
⊢ (𝜑 → inf(ran (𝑛 ∈
(ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < ) ∈ ℝ) |
130 | 33, 129 | eqeltrd 2838 |
1
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) |