Step | Hyp | Ref
| Expression |
1 | | mbflimsup.2 |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) |
2 | | mbflimsup.h |
. . . . . 6
⊢ 𝐻 = (𝑚 ∈ ℝ ↦ sup((((𝑛 ∈ 𝑍 ↦ 𝐵) “ (𝑚[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
3 | | mbflimsup.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 3 | fvexi 6557 |
. . . . . . . 8
⊢ 𝑍 ∈ V |
5 | 4 | mptex 6857 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V |
6 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V) |
7 | | uzssz 12118 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
8 | 3, 7 | eqsstri 3926 |
. . . . . . . 8
⊢ 𝑍 ⊆
ℤ |
9 | | zssre 11841 |
. . . . . . . 8
⊢ ℤ
⊆ ℝ |
10 | 8, 9 | sstri 3902 |
. . . . . . 7
⊢ 𝑍 ⊆
ℝ |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ⊆ ℝ) |
12 | | mbflimsup.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | 3 | uzsup 13086 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) =
+∞) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(𝑍, ℝ*, < ) =
+∞) |
15 | 14 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(𝑍, ℝ*, < ) =
+∞) |
16 | 2, 6, 11, 15 | limsupval2 14676 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) = inf((𝐻 “ 𝑍), ℝ*, <
)) |
17 | | imassrn 5822 |
. . . . . . 7
⊢ (𝐻 “ 𝑍) ⊆ ran 𝐻 |
18 | 12 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ ℤ) |
19 | | mbflimsup.6 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
20 | 19 | anass1rs 651 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℝ) |
21 | 20 | fmpttd 6747 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ) |
22 | | mbflimsup.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) |
23 | 22 | ltpnfd 12371 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) < +∞) |
24 | 2, 3 | limsupgre 14677 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ ∧ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) < +∞) → 𝐻:ℝ⟶ℝ) |
25 | 18, 21, 23, 24 | syl3anc 1364 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻:ℝ⟶ℝ) |
26 | 25 | frnd 6394 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐻 ⊆ ℝ) |
27 | 17, 26 | sstrid 3904 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) ⊆ ℝ) |
28 | 25 | fdmd 6396 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐻 = ℝ) |
29 | 28 | ineq1d 4112 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) = (ℝ ∩ 𝑍)) |
30 | | sseqin2 4116 |
. . . . . . . . . 10
⊢ (𝑍 ⊆ ℝ ↔ (ℝ
∩ 𝑍) = 𝑍) |
31 | 10, 30 | mpbi 231 |
. . . . . . . . 9
⊢ (ℝ
∩ 𝑍) = 𝑍 |
32 | 29, 31 | syl6eq 2847 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) = 𝑍) |
33 | | uzid 12113 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
34 | 12, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
35 | 34, 3 | syl6eleqr 2894 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
36 | 35 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ 𝑍) |
37 | 36 | ne0d 4225 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ≠ ∅) |
38 | 32, 37 | eqnetrd 3051 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) ≠ ∅) |
39 | | imadisj 5829 |
. . . . . . . 8
⊢ ((𝐻 “ 𝑍) = ∅ ↔ (dom 𝐻 ∩ 𝑍) = ∅) |
40 | 39 | necon3bii 3036 |
. . . . . . 7
⊢ ((𝐻 “ 𝑍) ≠ ∅ ↔ (dom 𝐻 ∩ 𝑍) ≠ ∅) |
41 | 38, 40 | sylibr 235 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) ≠ ∅) |
42 | 22 | leidd 11059 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) |
43 | 20 | rexrd 10542 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈
ℝ*) |
44 | 43 | fmpttd 6747 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) |
45 | 22 | rexrd 10542 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈
ℝ*) |
46 | 2 | limsuple 14674 |
. . . . . . . . . . 11
⊢ ((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ* ∧ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ*) → ((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
47 | 11, 44, 45, 46 | syl3anc 1364 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
48 | 42, 47 | mpbid 233 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦)) |
49 | | ssralv 3958 |
. . . . . . . . 9
⊢ (𝑍 ⊆ ℝ →
(∀𝑦 ∈ ℝ
(lim sup‘(𝑛 ∈
𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦) → ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
50 | 10, 48, 49 | mpsyl 68 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦)) |
51 | 2 | limsupgf 14671 |
. . . . . . . . . 10
⊢ 𝐻:ℝ⟶ℝ* |
52 | | ffn 6387 |
. . . . . . . . . 10
⊢ (𝐻:ℝ⟶ℝ* →
𝐻 Fn
ℝ) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝐻 Fn ℝ |
54 | | breq2 4970 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐻‘𝑦) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
55 | 54 | ralima 6870 |
. . . . . . . . 9
⊢ ((𝐻 Fn ℝ ∧ 𝑍 ⊆ ℝ) →
(∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
56 | 53, 11, 55 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
57 | 50, 56 | mpbird 258 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧) |
58 | | breq1 4969 |
. . . . . . . . 9
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (𝑦 ≤ 𝑧 ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧)) |
59 | 58 | ralbidv 3164 |
. . . . . . . 8
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧 ↔ ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧)) |
60 | 59 | rspcev 3559 |
. . . . . . 7
⊢ (((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ ∧ ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) |
61 | 22, 57, 60 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) |
62 | | infxrre 12584 |
. . . . . 6
⊢ (((𝐻 “ 𝑍) ⊆ ℝ ∧ (𝐻 “ 𝑍) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) → inf((𝐻 “ 𝑍), ℝ*, < ) = inf((𝐻 “ 𝑍), ℝ, < )) |
63 | 27, 41, 61, 62 | syl3anc 1364 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → inf((𝐻 “ 𝑍), ℝ*, < ) = inf((𝐻 “ 𝑍), ℝ, < )) |
64 | | df-ima 5461 |
. . . . . . 7
⊢ (𝐻 “ 𝑍) = ran (𝐻 ↾ 𝑍) |
65 | 25 | feqmptd 6606 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 = (𝑖 ∈ ℝ ↦ (𝐻‘𝑖))) |
66 | 65 | reseq1d 5738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍)) |
67 | | resmpt 5791 |
. . . . . . . . . . 11
⊢ (𝑍 ⊆ ℝ → ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖))) |
68 | 10, 67 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖)) |
69 | 66, 68 | syl6eq 2847 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖))) |
70 | 10 | sseli 3889 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ ℝ) |
71 | | ffvelrn 6719 |
. . . . . . . . . . . . 13
⊢ ((𝐻:ℝ⟶ℝ ∧
𝑖 ∈ ℝ) →
(𝐻‘𝑖) ∈ ℝ) |
72 | 25, 70, 71 | syl2an 595 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ∈ ℝ) |
73 | 72 | rexrd 10542 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ∈
ℝ*) |
74 | | simplll 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
75 | 3 | uztrn2 12116 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
76 | 75 | adantll 710 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
77 | | simpllr 772 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ 𝐴) |
78 | 74, 76, 77, 19 | syl12anc 833 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝐵 ∈ ℝ) |
79 | 78 | fmpttd 6747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ) |
80 | 79 | frnd 6394 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
81 | | eqid 2795 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) = (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) |
82 | 81, 78 | dmmptd 6366 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → dom (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) = (ℤ≥‘𝑖)) |
83 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
84 | 83, 3 | syl6eleq 2893 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
85 | | eluzelz 12108 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑖 ∈ ℤ) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
87 | 86 | adantlr 711 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
88 | | uzid 12113 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
(ℤ≥‘𝑖)) |
89 | | ne0i 4224 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈
(ℤ≥‘𝑖) → (ℤ≥‘𝑖) ≠ ∅) |
90 | 87, 88, 89 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ≠ ∅) |
91 | 82, 90 | eqnetrd 3051 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → dom (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
92 | | dm0rn0 5684 |
. . . . . . . . . . . . . . 15
⊢ (dom
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) = ∅ ↔ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) = ∅) |
93 | 92 | necon3bii 3036 |
. . . . . . . . . . . . . 14
⊢ (dom
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ↔ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
94 | 91, 93 | sylib 219 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
95 | 84 | adantlr 711 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
96 | | uzss 12119 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
98 | 97, 3 | syl6sseqr 3943 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ⊆ 𝑍) |
99 | 72 | leidd 11059 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ≤ (𝐻‘𝑖)) |
100 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑍 ⊆ ℝ) |
101 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) |
102 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
103 | 10, 102 | sseldi 3891 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℝ) |
104 | 2 | limsupgle 14673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ (𝐻‘𝑖) ∈ ℝ*) → ((𝐻‘𝑖) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
105 | 100, 101,
103, 73, 104 | syl211anc 1369 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((𝐻‘𝑖) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
106 | 99, 105 | mpbid 233 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
107 | | ssralv 3958 |
. . . . . . . . . . . . . . . . 17
⊢
((ℤ≥‘𝑖) ⊆ 𝑍 → (∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)) → ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
108 | 98, 106, 107 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
109 | 98 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) →
(ℤ≥‘𝑖) ⊆ 𝑍) |
110 | 109 | resmptd 5794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖)) = (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
111 | 110 | fveq1d 6545 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘)) |
112 | | fvres 6562 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(ℤ≥‘𝑖) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
113 | 112 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
114 | 111, 113 | eqtr3d 2833 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
115 | 114 | breq1d 4976 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
116 | | eluzle 12111 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈
(ℤ≥‘𝑖) → 𝑖 ≤ 𝑘) |
117 | 116 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → 𝑖 ≤ 𝑘) |
118 | | biimt 362 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ≤ 𝑘 → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
120 | 115, 119 | bitrd 280 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
121 | 120 | ralbidva 3163 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
122 | 108, 121 | mpbird 258 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)) |
123 | | ffn 6387 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ → (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖)) |
124 | | breq1 4969 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) → (𝑧 ≤ (𝐻‘𝑖) ↔ ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
125 | 124 | ralrn 6724 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
126 | 79, 123, 125 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
127 | 122, 126 | mpbird 258 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖)) |
128 | | brralrspcev 5026 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑖) ∈ ℝ ∧ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
129 | 72, 127, 128 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
130 | 80, 94, 129 | suprcld 11457 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
131 | 130 | rexrd 10542 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ*) |
132 | 80 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
133 | 94 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
134 | 129 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
135 | 8 | sseli 3889 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
136 | | eluz 12112 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈
(ℤ≥‘𝑖) ↔ 𝑖 ≤ 𝑘)) |
137 | 87, 135, 136 | syl2an 595 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑘 ∈ (ℤ≥‘𝑖) ↔ 𝑖 ≤ 𝑘)) |
138 | 137 | biimprd 249 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑖 ≤ 𝑘 → 𝑘 ∈ (ℤ≥‘𝑖))) |
139 | 138 | impr 455 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → 𝑘 ∈ (ℤ≥‘𝑖)) |
140 | 139, 114 | syldan 591 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
141 | 79 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ) |
142 | 141, 123 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖)) |
143 | | fnfvelrn 6718 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
144 | 142, 139,
143 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
145 | 140, 144 | eqeltrrd 2884 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
146 | 132, 133,
134, 145 | suprubd 11456 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
147 | 146 | expr 457 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
148 | 147 | ralrimiva 3149 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
149 | 2 | limsupgle 14673 |
. . . . . . . . . . . . 13
⊢ (((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ sup(ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ*) → ((𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )))) |
150 | 100, 101,
103, 131, 149 | syl211anc 1369 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )))) |
151 | 148, 150 | mpbird 258 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
152 | | suprleub 11460 |
. . . . . . . . . . . . 13
⊢ (((ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) ∧ (𝐻‘𝑖) ∈ ℝ) → (sup(ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
153 | 80, 94, 129, 72, 152 | syl31anc 1366 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
154 | 127, 153 | mpbird 258 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖)) |
155 | 73, 131, 151, 154 | xrletrid 12403 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) = sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
156 | 155 | mpteq2dva 5060 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖)) = (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
157 | 69, 156 | eqtrd 2831 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
158 | 157 | rneqd 5695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝐻 ↾ 𝑍) = ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
159 | 64, 158 | syl5eq 2843 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) = ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
160 | 159 | infeq1d 8792 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → inf((𝐻 “ 𝑍), ℝ, < ) = inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
161 | 16, 63, 160 | 3eqtrd 2835 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) = inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
162 | 161 | mpteq2dva 5060 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
))) |
163 | 1, 162 | syl5eq 2843 |
. 2
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
))) |
164 | | eqid 2795 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) =
(𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
165 | | eqid 2795 |
. . . 4
⊢
(ℤ≥‘𝑖) = (ℤ≥‘𝑖) |
166 | | eqid 2795 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
167 | | simpll 763 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
168 | 75 | adantll 710 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
169 | | mbflimsup.5 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
170 | 167, 168,
169 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
171 | | simpll 763 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝜑) |
172 | 75 | ad2ant2lr 744 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝑛 ∈ 𝑍) |
173 | | simprr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
174 | 171, 172,
173, 19 | syl12anc 833 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
175 | 78 | ralrimiva 3149 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ∈ ℝ) |
176 | | breq1 4969 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → (𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
177 | 81, 176 | ralrnmpt 6730 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(ℤ≥‘𝑖)𝐵 ∈ ℝ → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
178 | 175, 177 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
179 | 178 | rexbidv 3260 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
180 | 129, 179 | mpbid 233 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦) |
181 | 180 | an32s 648 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦) |
182 | 165, 166,
86, 170, 174, 181 | mbfsup 23953 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) ∈
MblFn) |
183 | 130 | an32s 648 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
184 | 183 | anasss 467 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
185 | 2 | limsuple 14674 |
. . . . . . . 8
⊢ ((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ* ∧ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ*) → ((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
186 | 11, 44, 45, 185 | syl3anc 1364 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
187 | 42, 186 | mpbid 233 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖)) |
188 | | ssralv 3958 |
. . . . . 6
⊢ (𝑍 ⊆ ℝ →
(∀𝑖 ∈ ℝ
(lim sup‘(𝑛 ∈
𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
189 | 10, 187, 188 | mpsyl 68 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖)) |
190 | 155 | breq2d 4978 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
191 | 190 | ralbidva 3163 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) ↔ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
192 | 189, 191 | mpbid 233 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
193 | | breq1 4969 |
. . . . . 6
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
194 | 193 | ralbidv 3164 |
. . . . 5
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
195 | 194 | rspcev 3559 |
. . . 4
⊢ (((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ ∧ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) → ∃𝑦 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
196 | 22, 192, 195 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
197 | 3, 164, 12, 182, 184, 196 | mbfinf 23954 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) ∈
MblFn) |
198 | 163, 197 | eqeltrd 2883 |
1
⊢ (𝜑 → 𝐺 ∈ MblFn) |