| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑚𝜑 |
| 2 | | smflimsuplem4.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 3 | | smflimsuplem4.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 4 | | smflimsuplem4.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
| 5 | 3, 4 | eluzelz2d 45424 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 6 | | eqid 2737 |
. . . 4
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
| 7 | | fvexd 6921 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
| 8 | | fvexd 6921 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
| 9 | 1, 2, 5, 3, 6, 7, 8 | limsupequzmpt 45744 |
. . 3
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ (ℤ≥‘𝑁) ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 10 | | smflimsuplem4.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑆 ∈ SAlg) |
| 12 | 3, 4 | uzssd2 45428 |
. . . . . . . . 9
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆ 𝑍) |
| 13 | 12 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑚 ∈ 𝑍) |
| 14 | | smflimsuplem4.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 15 | 14 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
| 16 | 13, 15 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
| 17 | | eqid 2737 |
. . . . . . 7
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
| 18 | 11, 16, 17 | smff 46747 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
| 19 | | smflimsuplem4.e |
. . . . . . . 8
⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
| 20 | | smflimsuplem4.h |
. . . . . . . 8
⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
| 21 | 3, 19, 20, 13 | smflimsuplem1 46835 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → dom (𝐻‘𝑚) ⊆ dom (𝐹‘𝑚)) |
| 22 | | smflimsuplem4.i |
. . . . . . . . 9
⊢ (𝜑 → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)dom (𝐻‘𝑛)) |
| 23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)dom (𝐻‘𝑛)) |
| 24 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑚 ∈ (ℤ≥‘𝑁)) |
| 25 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝐻‘𝑛) = (𝐻‘𝑚)) |
| 26 | 25 | dmeqd 5916 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → dom (𝐻‘𝑛) = dom (𝐻‘𝑚)) |
| 27 | 26 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑥 ∈ dom (𝐻‘𝑛) ↔ 𝑥 ∈ dom (𝐻‘𝑚))) |
| 28 | 23, 24, 27 | eliind 45076 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ dom (𝐻‘𝑚)) |
| 29 | 21, 28 | sseldd 3984 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
| 30 | 18, 29 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
| 31 | 30 | rexrd 11311 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑚)‘𝑥) ∈
ℝ*) |
| 32 | 1, 5, 6, 31 | limsupvaluzmpt 45732 |
. . 3
⊢ (𝜑 → (lim sup‘(𝑚 ∈
(ℤ≥‘𝑁) ↦ ((𝐹‘𝑚)‘𝑥))) = inf(ran (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
| 33 | 9, 32 | eqtrd 2777 |
. 2
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = inf(ran (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
| 34 | | smflimsuplem4.1 |
. . 3
⊢
Ⅎ𝑛𝜑 |
| 35 | 12 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) →
(ℤ≥‘𝑁) ⊆ 𝑍) |
| 36 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ (ℤ≥‘𝑁)) |
| 37 | 35, 36 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ 𝑍) |
| 38 | 20 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)))) |
| 39 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢ (𝐸‘𝑛) ∈ V |
| 40 | 39 | mptex 7243 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈
V |
| 41 | 40 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈
V) |
| 42 | 38, 41 | fvmpt2d 7029 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
| 43 | 37, 42 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
| 44 | 43 | dmeqd 5916 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝐻‘𝑛) = dom (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
| 45 | | xrltso 13183 |
. . . . . . . . . . . . 13
⊢ < Or
ℝ* |
| 46 | 45 | supex 9503 |
. . . . . . . . . . . 12
⊢ sup(ran
(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
V |
| 47 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
| 48 | 46, 47 | dmmpti 6712 |
. . . . . . . . . . 11
⊢ dom
(𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝐸‘𝑛) |
| 49 | 48 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝐸‘𝑛)) |
| 50 | 44, 49 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝐻‘𝑛) = (𝐸‘𝑛)) |
| 51 | 34, 50 | iineq2d 5015 |
. . . . . . . 8
⊢ (𝜑 → ∩ 𝑛 ∈ (ℤ≥‘𝑁)dom (𝐻‘𝑛) = ∩ 𝑛 ∈
(ℤ≥‘𝑁)(𝐸‘𝑛)) |
| 52 | 22, 51 | eleqtrd 2843 |
. . . . . . 7
⊢ (𝜑 → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)(𝐸‘𝑛)) |
| 53 | 52 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ ∩
𝑛 ∈
(ℤ≥‘𝑁)(𝐸‘𝑛)) |
| 54 | | eliinid 45116 |
. . . . . 6
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ (ℤ≥‘𝑁)(𝐸‘𝑛) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ (𝐸‘𝑛)) |
| 55 | 53, 36, 54 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ (𝐸‘𝑛)) |
| 56 | 46 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑥 ∈ (𝐸‘𝑛)) → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
V) |
| 57 | 43, 56 | fvmpt2d 7029 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑥 ∈ (𝐸‘𝑛)) → ((𝐻‘𝑛)‘𝑥) = sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
| 58 | 55, 57 | mpdan 687 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) = sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
| 59 | | eqid 2737 |
. . . . . . . . . 10
⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} = {𝑥 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} |
| 60 | 3 | eluzelz2 45414 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
| 61 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
| 62 | 60, 61 | uzn0d 45436 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ≠ ∅) |
| 63 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑚) ∈ V |
| 64 | 63 | dmex 7931 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐹‘𝑚) ∈ V |
| 65 | 64 | rgenw 3065 |
. . . . . . . . . . . . 13
⊢
∀𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V |
| 66 | 65 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
| 67 | 62, 66 | iinexd 45138 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
| 68 | 67 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) |
| 69 | 59, 68 | rabexd 5340 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) |
| 70 | 37, 69 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) |
| 71 | 19 | fvmpt2 7027 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ∧ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) → (𝐸‘𝑛) = {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
| 72 | 37, 70, 71 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐸‘𝑛) = {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
| 73 | 55, 72 | eleqtrd 2843 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
| 74 | | rabid 3458 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ↔ (𝑥 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ)) |
| 75 | 73, 74 | sylib 218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ)) |
| 76 | 75 | simprd 495 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ) |
| 77 | 58, 76 | eqeltrd 2841 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) ∈ ℝ) |
| 78 | 34, 58 | mpteq2da 5240 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) = (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
| 79 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
| 80 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑘)) |
| 81 | 80 | mpteq1d 5237 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥))) |
| 82 | 81 | rneqd 5949 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥))) |
| 83 | 82 | supeq1d 9486 |
. . . . 5
⊢ (𝑛 = 𝑘 → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) = sup(ran
(𝑚 ∈
(ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) |
| 84 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑚(𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) |
| 85 | | eluzelz 12888 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → 𝑛 ∈ ℤ) |
| 86 | 85 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 ∈ ℤ) |
| 87 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 = (𝑛 + 1)) |
| 88 | 86 | peano2zd 12725 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → (𝑛 + 1) ∈ ℤ) |
| 89 | 87, 88 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 ∈ ℤ) |
| 90 | 86 | zred 12722 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 ∈ ℝ) |
| 91 | 89 | zred 12722 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 ∈ ℝ) |
| 92 | 90 | ltp1d 12198 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 < (𝑛 + 1)) |
| 93 | 87 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → (𝑛 + 1) = 𝑘) |
| 94 | 92, 93 | breqtrd 5169 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 < 𝑘) |
| 95 | 90, 91, 94 | ltled 11409 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑛 ≤ 𝑘) |
| 96 | 61, 86, 89, 95 | eluzd 45420 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → 𝑘 ∈ (ℤ≥‘𝑛)) |
| 97 | | uzss 12901 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → (ℤ≥‘𝑘) ⊆
(ℤ≥‘𝑛)) |
| 98 | 96, 97 | syl 17 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) →
(ℤ≥‘𝑘) ⊆ (ℤ≥‘𝑛)) |
| 99 | | fvexd 6921 |
. . . . . . . 8
⊢ (((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
| 100 | 84, 98, 99 | rnmptss2 45264 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) |
| 101 | 100 | 3adant1 1131 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) |
| 102 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) |
| 103 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) |
| 104 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
| 105 | 37, 104 | syldanl 602 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
| 106 | 6 | uztrn2 12897 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑁)) |
| 107 | 106 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑁)) |
| 108 | 105, 107,
30 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
| 109 | 102, 103,
108 | rnmptssd 45201 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆ ℝ) |
| 110 | | ressxr 11305 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
| 111 | 110 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ℝ ⊆
ℝ*) |
| 112 | 109, 111 | sstrd 3994 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆
ℝ*) |
| 113 | 112 | 3adant3 1133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁) ∧ 𝑘 = (𝑛 + 1)) → ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) ⊆
ℝ*) |
| 114 | | supxrss 13374 |
. . . . . 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 6920 |
. . . . . . . . 9
⊢ 𝑍 ∈ V |
| 118 | 117 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ V) |
| 119 | | fvexd 6921 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛)‘𝑥) ∈ V) |
| 120 | | fvexd 6921 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘𝑁) ∈ V) |
| 121 | 34, 36 | ssdf 45080 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑁)) |
| 122 | | fvexd 6921 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) ∈ V) |
| 123 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐻‘𝑛)‘𝑥) = ((𝐻‘𝑛)‘𝑥)) |
| 124 | 34, 5, 6, 118, 12, 119, 120, 121, 122, 123 | climeldmeqmpt 45683 |
. . . . . . 7
⊢ (𝜑 → ((𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ ↔ (𝑛 ∈
(ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ )) |
| 125 | 116, 124 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ ) |
| 126 | 78, 125 | eqeltrrd 2842 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈ dom
⇝ ) |
| 127 | 34, 79, 5, 6, 76, 83, 115, 126 | climinf2mpt 45729 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ⇝
inf(ran (𝑛 ∈
(ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
| 128 | 78, 127 | eqbrtrd 5165 |
. . 3
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑥)) ⇝ inf(ran (𝑛 ∈ (ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < )) |
| 129 | 34, 5, 6, 77, 128 | climreclmpt 45699 |
. 2
⊢ (𝜑 → inf(ran (𝑛 ∈
(ℤ≥‘𝑁) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )),
ℝ*, < ) ∈ ℝ) |
| 130 | 33, 129 | eqeltrd 2841 |
1
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) |