Step | Hyp | Ref
| Expression |
1 | | mbflimsup.2 |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) |
2 | | mbflimsup.h |
. . . . . 6
⊢ 𝐻 = (𝑚 ∈ ℝ ↦ sup((((𝑛 ∈ 𝑍 ↦ 𝐵) “ (𝑚[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
3 | | mbflimsup.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | | fvex 6113 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ∈ V |
5 | 3, 4 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑍 ∈ V |
6 | 5 | mptex 6390 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V |
7 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V) |
8 | | uzssz 11583 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
9 | 3, 8 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝑍 ⊆
ℤ |
10 | | zssre 11261 |
. . . . . . . 8
⊢ ℤ
⊆ ℝ |
11 | 9, 10 | sstri 3577 |
. . . . . . 7
⊢ 𝑍 ⊆
ℝ |
12 | 11 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ⊆ ℝ) |
13 | | mbflimsup.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
14 | 3 | uzsup 12524 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) =
+∞) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(𝑍, ℝ*, < ) =
+∞) |
16 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(𝑍, ℝ*, < ) =
+∞) |
17 | 2, 7, 12, 16 | limsupval2 14059 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) = inf((𝐻 “ 𝑍), ℝ*, <
)) |
18 | | imassrn 5396 |
. . . . . . 7
⊢ (𝐻 “ 𝑍) ⊆ ran 𝐻 |
19 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ ℤ) |
20 | | mbflimsup.6 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
21 | 20 | anass1rs 845 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℝ) |
22 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) = (𝑛 ∈ 𝑍 ↦ 𝐵) |
23 | 21, 22 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ) |
24 | | mbflimsup.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) |
25 | 24 | ltpnfd 11831 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) < +∞) |
26 | 2, 3 | limsupgre 14060 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ ∧ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) < +∞) → 𝐻:ℝ⟶ℝ) |
27 | 19, 23, 25, 26 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻:ℝ⟶ℝ) |
28 | | frn 5966 |
. . . . . . . 8
⊢ (𝐻:ℝ⟶ℝ →
ran 𝐻 ⊆
ℝ) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐻 ⊆ ℝ) |
30 | 18, 29 | syl5ss 3579 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) ⊆ ℝ) |
31 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐻:ℝ⟶ℝ →
dom 𝐻 =
ℝ) |
32 | 27, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐻 = ℝ) |
33 | 32 | ineq1d 3775 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) = (ℝ ∩ 𝑍)) |
34 | | sseqin2 3779 |
. . . . . . . . . 10
⊢ (𝑍 ⊆ ℝ ↔ (ℝ
∩ 𝑍) = 𝑍) |
35 | 11, 34 | mpbi 219 |
. . . . . . . . 9
⊢ (ℝ
∩ 𝑍) = 𝑍 |
36 | 33, 35 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) = 𝑍) |
37 | | uzid 11578 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
38 | 13, 37 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
39 | 38, 3 | syl6eleqr 2699 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
40 | 39 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ 𝑍) |
41 | | ne0i 3880 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝑍 → 𝑍 ≠ ∅) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ≠ ∅) |
43 | 36, 42 | eqnetrd 2849 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) ≠ ∅) |
44 | | imadisj 5403 |
. . . . . . . 8
⊢ ((𝐻 “ 𝑍) = ∅ ↔ (dom 𝐻 ∩ 𝑍) = ∅) |
45 | 44 | necon3bii 2834 |
. . . . . . 7
⊢ ((𝐻 “ 𝑍) ≠ ∅ ↔ (dom 𝐻 ∩ 𝑍) ≠ ∅) |
46 | 43, 45 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) ≠ ∅) |
47 | 24 | leidd 10473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) |
48 | 21 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈
ℝ*) |
49 | 48, 22 | fmptd 6292 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) |
50 | 24 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈
ℝ*) |
51 | 2 | limsuple 14057 |
. . . . . . . . . . 11
⊢ ((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ* ∧ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ*) → ((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
52 | 12, 49, 50, 51 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
53 | 47, 52 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦)) |
54 | | ssralv 3629 |
. . . . . . . . 9
⊢ (𝑍 ⊆ ℝ →
(∀𝑦 ∈ ℝ
(lim sup‘(𝑛 ∈
𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦) → ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
55 | 11, 53, 54 | mpsyl 66 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦)) |
56 | 2 | limsupgf 14054 |
. . . . . . . . . 10
⊢ 𝐻:ℝ⟶ℝ* |
57 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐻:ℝ⟶ℝ* →
𝐻 Fn
ℝ) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝐻 Fn ℝ |
59 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐻‘𝑦) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
60 | 59 | ralima 6402 |
. . . . . . . . 9
⊢ ((𝐻 Fn ℝ ∧ 𝑍 ⊆ ℝ) →
(∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
61 | 58, 12, 60 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
62 | 55, 61 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧) |
63 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (𝑦 ≤ 𝑧 ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧)) |
64 | 63 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧 ↔ ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧)) |
65 | 64 | rspcev 3282 |
. . . . . . 7
⊢ (((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ ∧ ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) |
66 | 24, 62, 65 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) |
67 | | infxrre 12038 |
. . . . . 6
⊢ (((𝐻 “ 𝑍) ⊆ ℝ ∧ (𝐻 “ 𝑍) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) → inf((𝐻 “ 𝑍), ℝ*, < ) = inf((𝐻 “ 𝑍), ℝ, < )) |
68 | 30, 46, 66, 67 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → inf((𝐻 “ 𝑍), ℝ*, < ) = inf((𝐻 “ 𝑍), ℝ, < )) |
69 | | df-ima 5051 |
. . . . . . 7
⊢ (𝐻 “ 𝑍) = ran (𝐻 ↾ 𝑍) |
70 | 27 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 = (𝑖 ∈ ℝ ↦ (𝐻‘𝑖))) |
71 | 70 | reseq1d 5316 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍)) |
72 | | resmpt 5369 |
. . . . . . . . . . 11
⊢ (𝑍 ⊆ ℝ → ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖))) |
73 | 11, 72 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖)) |
74 | 71, 73 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖))) |
75 | 11 | sseli 3564 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ ℝ) |
76 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝐻:ℝ⟶ℝ ∧
𝑖 ∈ ℝ) →
(𝐻‘𝑖) ∈ ℝ) |
77 | 27, 75, 76 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ∈ ℝ) |
78 | 77 | rexrd 9968 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ∈
ℝ*) |
79 | | simplll 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
80 | 3 | uztrn2 11581 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
81 | 80 | adantll 746 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
82 | | simpllr 795 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ 𝐴) |
83 | 79, 81, 82, 20 | syl12anc 1316 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝐵 ∈ ℝ) |
84 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) = (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) |
85 | 83, 84 | fmptd 6292 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ) |
86 | | frn 5966 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ → ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
88 | 84, 83 | dmmptd 5937 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → dom (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) = (ℤ≥‘𝑖)) |
89 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
90 | 89, 3 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
91 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑖 ∈ ℤ) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
93 | 92 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
94 | | uzid 11578 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
(ℤ≥‘𝑖)) |
95 | | ne0i 3880 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈
(ℤ≥‘𝑖) → (ℤ≥‘𝑖) ≠ ∅) |
96 | 93, 94, 95 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ≠ ∅) |
97 | 88, 96 | eqnetrd 2849 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → dom (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
98 | | dm0rn0 5263 |
. . . . . . . . . . . . . . 15
⊢ (dom
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) = ∅ ↔ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) = ∅) |
99 | 98 | necon3bii 2834 |
. . . . . . . . . . . . . 14
⊢ (dom
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ↔ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
100 | 97, 99 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
101 | 90 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
102 | | uzss 11584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
104 | 103, 3 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ⊆ 𝑍) |
105 | 77 | leidd 10473 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ≤ (𝐻‘𝑖)) |
106 | 11 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑍 ⊆ ℝ) |
107 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) |
108 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
109 | 11, 108 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℝ) |
110 | 2 | limsupgle 14056 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ (𝐻‘𝑖) ∈ ℝ*) → ((𝐻‘𝑖) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
111 | 106, 107,
109, 78, 110 | syl211anc 1324 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((𝐻‘𝑖) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
112 | 105, 111 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
113 | | ssralv 3629 |
. . . . . . . . . . . . . . . . 17
⊢
((ℤ≥‘𝑖) ⊆ 𝑍 → (∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)) → ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
114 | 104, 112,
113 | sylc 63 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
115 | 104 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) →
(ℤ≥‘𝑖) ⊆ 𝑍) |
116 | 115 | resmptd 5371 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖)) = (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
117 | 116 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘)) |
118 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(ℤ≥‘𝑖) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
119 | 118 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
120 | 117, 119 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
121 | 120 | breq1d 4593 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
122 | | eluzle 11576 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈
(ℤ≥‘𝑖) → 𝑖 ≤ 𝑘) |
123 | 122 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → 𝑖 ≤ 𝑘) |
124 | | biimt 349 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ≤ 𝑘 → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
126 | 121, 125 | bitrd 267 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
127 | 126 | ralbidva 2968 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
128 | 114, 127 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)) |
129 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ → (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖)) |
130 | | breq1 4586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) → (𝑧 ≤ (𝐻‘𝑖) ↔ ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
131 | 130 | ralrn 6270 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
132 | 85, 129, 131 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
133 | 128, 132 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖)) |
134 | | breq2 4587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝐻‘𝑖) → (𝑧 ≤ 𝑦 ↔ 𝑧 ≤ (𝐻‘𝑖))) |
135 | 134 | ralbidv 2969 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐻‘𝑖) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
136 | 135 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑖) ∈ ℝ ∧ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
137 | 77, 133, 136 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
138 | | suprcl 10862 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
139 | 87, 100, 137, 138 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
140 | 139 | rexrd 9968 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ*) |
141 | 87 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
142 | 100 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
143 | 137 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
144 | 9 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
145 | | eluz 11577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈
(ℤ≥‘𝑖) ↔ 𝑖 ≤ 𝑘)) |
146 | 93, 144, 145 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑘 ∈ (ℤ≥‘𝑖) ↔ 𝑖 ≤ 𝑘)) |
147 | 146 | biimprd 237 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑖 ≤ 𝑘 → 𝑘 ∈ (ℤ≥‘𝑖))) |
148 | 147 | impr 647 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → 𝑘 ∈ (ℤ≥‘𝑖)) |
149 | 148, 120 | syldan 486 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
150 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ) |
151 | 150, 129 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖)) |
152 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
153 | 151, 148,
152 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
154 | 149, 153 | eqeltrrd 2689 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
155 | | suprub 10863 |
. . . . . . . . . . . . . . 15
⊢ (((ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) ∧ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
156 | 141, 142,
143, 154, 155 | syl31anc 1321 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
157 | 156 | expr 641 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
158 | 157 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
159 | 2 | limsupgle 14056 |
. . . . . . . . . . . . 13
⊢ (((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ sup(ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ*) → ((𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )))) |
160 | 106, 107,
109, 140, 159 | syl211anc 1324 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )))) |
161 | 158, 160 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
162 | | suprleub 10866 |
. . . . . . . . . . . . 13
⊢ (((ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) ∧ (𝐻‘𝑖) ∈ ℝ) → (sup(ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
163 | 87, 100, 137, 77, 162 | syl31anc 1321 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
164 | 133, 163 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖)) |
165 | 78, 140, 161, 164 | xrletrid 11862 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) = sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
166 | 165 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖)) = (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
167 | 74, 166 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
168 | 167 | rneqd 5274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝐻 ↾ 𝑍) = ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
169 | 69, 168 | syl5eq 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) = ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
170 | 169 | infeq1d 8266 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → inf((𝐻 “ 𝑍), ℝ, < ) = inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
171 | 17, 68, 170 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) = inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
172 | 171 | mpteq2dva 4672 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
))) |
173 | 1, 172 | syl5eq 2656 |
. 2
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
))) |
174 | | eqid 2610 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) =
(𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
175 | | eqid 2610 |
. . . 4
⊢
(ℤ≥‘𝑖) = (ℤ≥‘𝑖) |
176 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
177 | | simpll 786 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
178 | 80 | adantll 746 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
179 | | mbflimsup.5 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
180 | 177, 178,
179 | syl2anc 691 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
181 | | simpll 786 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝜑) |
182 | 80 | ad2ant2lr 780 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝑛 ∈ 𝑍) |
183 | | simprr 792 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
184 | 181, 182,
183, 20 | syl12anc 1316 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
185 | 83 | ralrimiva 2949 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ∈ ℝ) |
186 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → (𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
187 | 84, 186 | ralrnmpt 6276 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(ℤ≥‘𝑖)𝐵 ∈ ℝ → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
188 | 185, 187 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
189 | 188 | rexbidv 3034 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
190 | 137, 189 | mpbid 221 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦) |
191 | 190 | an32s 842 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦) |
192 | 175, 176,
92, 180, 184, 191 | mbfsup 23237 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) ∈
MblFn) |
193 | 139 | an32s 842 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
194 | 193 | anasss 677 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
195 | 2 | limsuple 14057 |
. . . . . . . 8
⊢ ((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ* ∧ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ*) → ((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
196 | 12, 49, 50, 195 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
197 | 47, 196 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖)) |
198 | | ssralv 3629 |
. . . . . 6
⊢ (𝑍 ⊆ ℝ →
(∀𝑖 ∈ ℝ
(lim sup‘(𝑛 ∈
𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
199 | 11, 197, 198 | mpsyl 66 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖)) |
200 | 165 | breq2d 4595 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
201 | 200 | ralbidva 2968 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) ↔ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
202 | 199, 201 | mpbid 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
203 | | breq1 4586 |
. . . . . 6
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
204 | 203 | ralbidv 2969 |
. . . . 5
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
205 | 204 | rspcev 3282 |
. . . 4
⊢ (((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ ∧ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) → ∃𝑦 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
206 | 24, 202, 205 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
207 | 3, 174, 13, 192, 194, 206 | mbfinf 23238 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) ∈
MblFn) |
208 | 173, 207 | eqeltrd 2688 |
1
⊢ (𝜑 → 𝐺 ∈ MblFn) |