Step | Hyp | Ref
| Expression |
1 | | mbflimsup.2 |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) |
2 | | mbflimsup.h |
. . . . . 6
⊢ 𝐻 = (𝑚 ∈ ℝ ↦ sup((((𝑛 ∈ 𝑍 ↦ 𝐵) “ (𝑚[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
3 | | mbflimsup.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 3 | fvexi 6731 |
. . . . . . . 8
⊢ 𝑍 ∈ V |
5 | 4 | mptex 7039 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V |
6 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V) |
7 | | uzssz 12459 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
8 | 3, 7 | eqsstri 3935 |
. . . . . . . 8
⊢ 𝑍 ⊆
ℤ |
9 | | zssre 12183 |
. . . . . . . 8
⊢ ℤ
⊆ ℝ |
10 | 8, 9 | sstri 3910 |
. . . . . . 7
⊢ 𝑍 ⊆
ℝ |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ⊆ ℝ) |
12 | | mbflimsup.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | 3 | uzsup 13436 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) =
+∞) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(𝑍, ℝ*, < ) =
+∞) |
15 | 14 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(𝑍, ℝ*, < ) =
+∞) |
16 | 2, 6, 11, 15 | limsupval2 15041 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) = inf((𝐻 “ 𝑍), ℝ*, <
)) |
17 | | imassrn 5940 |
. . . . . . 7
⊢ (𝐻 “ 𝑍) ⊆ ran 𝐻 |
18 | 12 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ ℤ) |
19 | | mbflimsup.6 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
20 | 19 | anass1rs 655 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℝ) |
21 | 20 | fmpttd 6932 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ) |
22 | | mbflimsup.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) |
23 | 22 | ltpnfd 12713 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) < +∞) |
24 | 2, 3 | limsupgre 15042 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ ∧ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) < +∞) → 𝐻:ℝ⟶ℝ) |
25 | 18, 21, 23, 24 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻:ℝ⟶ℝ) |
26 | 25 | frnd 6553 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐻 ⊆ ℝ) |
27 | 17, 26 | sstrid 3912 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) ⊆ ℝ) |
28 | 25 | fdmd 6556 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐻 = ℝ) |
29 | 28 | ineq1d 4126 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) = (ℝ ∩ 𝑍)) |
30 | | sseqin2 4130 |
. . . . . . . . . 10
⊢ (𝑍 ⊆ ℝ ↔ (ℝ
∩ 𝑍) = 𝑍) |
31 | 10, 30 | mpbi 233 |
. . . . . . . . 9
⊢ (ℝ
∩ 𝑍) = 𝑍 |
32 | 29, 31 | eqtrdi 2794 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) = 𝑍) |
33 | | uzid 12453 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
34 | 12, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
35 | 34, 3 | eleqtrrdi 2849 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
36 | 35 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ 𝑍) |
37 | 36 | ne0d 4250 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ≠ ∅) |
38 | 32, 37 | eqnetrd 3008 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) ≠ ∅) |
39 | | imadisj 5948 |
. . . . . . . 8
⊢ ((𝐻 “ 𝑍) = ∅ ↔ (dom 𝐻 ∩ 𝑍) = ∅) |
40 | 39 | necon3bii 2993 |
. . . . . . 7
⊢ ((𝐻 “ 𝑍) ≠ ∅ ↔ (dom 𝐻 ∩ 𝑍) ≠ ∅) |
41 | 38, 40 | sylibr 237 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) ≠ ∅) |
42 | 22 | leidd 11398 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) |
43 | 20 | rexrd 10883 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈
ℝ*) |
44 | 43 | fmpttd 6932 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) |
45 | 22 | rexrd 10883 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈
ℝ*) |
46 | 2 | limsuple 15039 |
. . . . . . . . . . 11
⊢ ((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ* ∧ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ*) → ((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
47 | 11, 44, 45, 46 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
48 | 42, 47 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦)) |
49 | | ssralv 3967 |
. . . . . . . . 9
⊢ (𝑍 ⊆ ℝ →
(∀𝑦 ∈ ℝ
(lim sup‘(𝑛 ∈
𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦) → ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
50 | 10, 48, 49 | mpsyl 68 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦)) |
51 | 2 | limsupgf 15036 |
. . . . . . . . . 10
⊢ 𝐻:ℝ⟶ℝ* |
52 | | ffn 6545 |
. . . . . . . . . 10
⊢ (𝐻:ℝ⟶ℝ* →
𝐻 Fn
ℝ) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝐻 Fn ℝ |
54 | | breq2 5057 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐻‘𝑦) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
55 | 54 | ralima 7054 |
. . . . . . . . 9
⊢ ((𝐻 Fn ℝ ∧ 𝑍 ⊆ ℝ) →
(∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
56 | 53, 11, 55 | sylancr 590 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
57 | 50, 56 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧) |
58 | | breq1 5056 |
. . . . . . . . 9
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (𝑦 ≤ 𝑧 ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧)) |
59 | 58 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧 ↔ ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧)) |
60 | 59 | rspcev 3537 |
. . . . . . 7
⊢ (((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ ∧ ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) |
61 | 22, 57, 60 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) |
62 | | infxrre 12926 |
. . . . . 6
⊢ (((𝐻 “ 𝑍) ⊆ ℝ ∧ (𝐻 “ 𝑍) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) → inf((𝐻 “ 𝑍), ℝ*, < ) = inf((𝐻 “ 𝑍), ℝ, < )) |
63 | 27, 41, 61, 62 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → inf((𝐻 “ 𝑍), ℝ*, < ) = inf((𝐻 “ 𝑍), ℝ, < )) |
64 | | df-ima 5564 |
. . . . . . 7
⊢ (𝐻 “ 𝑍) = ran (𝐻 ↾ 𝑍) |
65 | 25 | feqmptd 6780 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 = (𝑖 ∈ ℝ ↦ (𝐻‘𝑖))) |
66 | 65 | reseq1d 5850 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍)) |
67 | | resmpt 5905 |
. . . . . . . . . . 11
⊢ (𝑍 ⊆ ℝ → ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖))) |
68 | 10, 67 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖)) |
69 | 66, 68 | eqtrdi 2794 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖))) |
70 | 10 | sseli 3896 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ ℝ) |
71 | | ffvelrn 6902 |
. . . . . . . . . . . . 13
⊢ ((𝐻:ℝ⟶ℝ ∧
𝑖 ∈ ℝ) →
(𝐻‘𝑖) ∈ ℝ) |
72 | 25, 70, 71 | syl2an 599 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ∈ ℝ) |
73 | 72 | rexrd 10883 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ∈
ℝ*) |
74 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
75 | 3 | uztrn2 12457 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
76 | 75 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
77 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ 𝐴) |
78 | 74, 76, 77, 19 | syl12anc 837 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝐵 ∈ ℝ) |
79 | 78 | fmpttd 6932 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ) |
80 | 79 | frnd 6553 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
81 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) = (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) |
82 | 81, 78 | dmmptd 6523 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → dom (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) = (ℤ≥‘𝑖)) |
83 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
84 | 83, 3 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
85 | | eluzelz 12448 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑖 ∈ ℤ) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
87 | 86 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
88 | | uzid 12453 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
(ℤ≥‘𝑖)) |
89 | | ne0i 4249 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈
(ℤ≥‘𝑖) → (ℤ≥‘𝑖) ≠ ∅) |
90 | 87, 88, 89 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ≠ ∅) |
91 | 82, 90 | eqnetrd 3008 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → dom (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
92 | | dm0rn0 5794 |
. . . . . . . . . . . . . . 15
⊢ (dom
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) = ∅ ↔ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) = ∅) |
93 | 92 | necon3bii 2993 |
. . . . . . . . . . . . . 14
⊢ (dom
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ↔ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
94 | 91, 93 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
95 | 84 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
96 | | uzss 12461 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
98 | 97, 3 | sseqtrrdi 3952 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ⊆ 𝑍) |
99 | 72 | leidd 11398 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ≤ (𝐻‘𝑖)) |
100 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑍 ⊆ ℝ) |
101 | 44 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) |
102 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
103 | 10, 102 | sseldi 3899 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℝ) |
104 | 2 | limsupgle 15038 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ (𝐻‘𝑖) ∈ ℝ*) → ((𝐻‘𝑖) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
105 | 100, 101,
103, 73, 104 | syl211anc 1378 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((𝐻‘𝑖) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
106 | 99, 105 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
107 | | ssralv 3967 |
. . . . . . . . . . . . . . . . 17
⊢
((ℤ≥‘𝑖) ⊆ 𝑍 → (∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)) → ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
108 | 98, 106, 107 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
109 | 98 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) →
(ℤ≥‘𝑖) ⊆ 𝑍) |
110 | 109 | resmptd 5908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖)) = (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
111 | 110 | fveq1d 6719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘)) |
112 | | fvres 6736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(ℤ≥‘𝑖) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
113 | 112 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
114 | 111, 113 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
115 | 114 | breq1d 5063 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
116 | | eluzle 12451 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈
(ℤ≥‘𝑖) → 𝑖 ≤ 𝑘) |
117 | 116 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → 𝑖 ≤ 𝑘) |
118 | | biimt 364 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ≤ 𝑘 → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
120 | 115, 119 | bitrd 282 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
121 | 120 | ralbidva 3117 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
122 | 108, 121 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)) |
123 | | ffn 6545 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ → (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖)) |
124 | | breq1 5056 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) → (𝑧 ≤ (𝐻‘𝑖) ↔ ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
125 | 124 | ralrn 6907 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
126 | 79, 123, 125 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
127 | 122, 126 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖)) |
128 | | brralrspcev 5113 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑖) ∈ ℝ ∧ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
129 | 72, 127, 128 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
130 | 80, 94, 129 | suprcld 11795 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
131 | 130 | rexrd 10883 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ*) |
132 | 80 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
133 | 94 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
134 | 129 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
135 | 8 | sseli 3896 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
136 | | eluz 12452 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈
(ℤ≥‘𝑖) ↔ 𝑖 ≤ 𝑘)) |
137 | 87, 135, 136 | syl2an 599 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑘 ∈ (ℤ≥‘𝑖) ↔ 𝑖 ≤ 𝑘)) |
138 | 137 | biimprd 251 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑖 ≤ 𝑘 → 𝑘 ∈ (ℤ≥‘𝑖))) |
139 | 138 | impr 458 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → 𝑘 ∈ (ℤ≥‘𝑖)) |
140 | 139, 114 | syldan 594 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
141 | 79 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ) |
142 | 141, 123 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖)) |
143 | | fnfvelrn 6901 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
144 | 142, 139,
143 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
145 | 140, 144 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
146 | 132, 133,
134, 145 | suprubd 11794 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
147 | 146 | expr 460 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
148 | 147 | ralrimiva 3105 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
149 | 2 | limsupgle 15038 |
. . . . . . . . . . . . 13
⊢ (((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ sup(ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ*) → ((𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )))) |
150 | 100, 101,
103, 131, 149 | syl211anc 1378 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )))) |
151 | 148, 150 | mpbird 260 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
152 | | suprleub 11798 |
. . . . . . . . . . . . 13
⊢ (((ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) ∧ (𝐻‘𝑖) ∈ ℝ) → (sup(ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
153 | 80, 94, 129, 72, 152 | syl31anc 1375 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
154 | 127, 153 | mpbird 260 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖)) |
155 | 73, 131, 151, 154 | xrletrid 12745 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) = sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
156 | 155 | mpteq2dva 5150 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖)) = (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
157 | 69, 156 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
158 | 157 | rneqd 5807 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝐻 ↾ 𝑍) = ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
159 | 64, 158 | syl5eq 2790 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) = ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
160 | 159 | infeq1d 9093 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → inf((𝐻 “ 𝑍), ℝ, < ) = inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
161 | 16, 63, 160 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) = inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
162 | 161 | mpteq2dva 5150 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
))) |
163 | 1, 162 | syl5eq 2790 |
. 2
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
))) |
164 | | eqid 2737 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) =
(𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
165 | | eqid 2737 |
. . . 4
⊢
(ℤ≥‘𝑖) = (ℤ≥‘𝑖) |
166 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
167 | | simpll 767 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
168 | 75 | adantll 714 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
169 | | mbflimsup.5 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
170 | 167, 168,
169 | syl2anc 587 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
171 | | simpll 767 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝜑) |
172 | 75 | ad2ant2lr 748 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝑛 ∈ 𝑍) |
173 | | simprr 773 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
174 | 171, 172,
173, 19 | syl12anc 837 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
175 | 78 | ralrimiva 3105 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ∈ ℝ) |
176 | | breq1 5056 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → (𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
177 | 81, 176 | ralrnmptw 6913 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(ℤ≥‘𝑖)𝐵 ∈ ℝ → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
178 | 175, 177 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
179 | 178 | rexbidv 3216 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
180 | 129, 179 | mpbid 235 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦) |
181 | 180 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦) |
182 | 165, 166,
86, 170, 174, 181 | mbfsup 24561 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) ∈
MblFn) |
183 | 130 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
184 | 183 | anasss 470 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
185 | 2 | limsuple 15039 |
. . . . . . . 8
⊢ ((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ* ∧ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ*) → ((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
186 | 11, 44, 45, 185 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
187 | 42, 186 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖)) |
188 | | ssralv 3967 |
. . . . . 6
⊢ (𝑍 ⊆ ℝ →
(∀𝑖 ∈ ℝ
(lim sup‘(𝑛 ∈
𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
189 | 10, 187, 188 | mpsyl 68 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖)) |
190 | 155 | breq2d 5065 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
191 | 190 | ralbidva 3117 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) ↔ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
192 | 189, 191 | mpbid 235 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
193 | | breq1 5056 |
. . . . . 6
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
194 | 193 | ralbidv 3118 |
. . . . 5
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
195 | 194 | rspcev 3537 |
. . . 4
⊢ (((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ ∧ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) → ∃𝑦 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
196 | 22, 192, 195 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
197 | 3, 164, 12, 182, 184, 196 | mbfinf 24562 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) ∈
MblFn) |
198 | 163, 197 | eqeltrd 2838 |
1
⊢ (𝜑 → 𝐺 ∈ MblFn) |