Step | Hyp | Ref
| Expression |
1 | | mbflimsup.2 |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) |
2 | | mbflimsup.h |
. . . . . 6
⊢ 𝐻 = (𝑚 ∈ ℝ ↦ sup((((𝑛 ∈ 𝑍 ↦ 𝐵) “ (𝑚[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
3 | | mbflimsup.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 3 | fvexi 6345 |
. . . . . . . 8
⊢ 𝑍 ∈ V |
5 | 4 | mptex 6632 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V |
6 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V) |
7 | | uzssz 11912 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
8 | 3, 7 | eqsstri 3784 |
. . . . . . . 8
⊢ 𝑍 ⊆
ℤ |
9 | | zssre 11590 |
. . . . . . . 8
⊢ ℤ
⊆ ℝ |
10 | 8, 9 | sstri 3761 |
. . . . . . 7
⊢ 𝑍 ⊆
ℝ |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ⊆ ℝ) |
12 | | mbflimsup.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | 3 | uzsup 12869 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) =
+∞) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(𝑍, ℝ*, < ) =
+∞) |
15 | 14 | adantr 466 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(𝑍, ℝ*, < ) =
+∞) |
16 | 2, 6, 11, 15 | limsupval2 14418 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) = inf((𝐻 “ 𝑍), ℝ*, <
)) |
17 | | imassrn 5617 |
. . . . . . 7
⊢ (𝐻 “ 𝑍) ⊆ ran 𝐻 |
18 | 12 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ ℤ) |
19 | | mbflimsup.6 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
20 | 19 | anass1rs 634 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℝ) |
21 | | eqid 2771 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) = (𝑛 ∈ 𝑍 ↦ 𝐵) |
22 | 20, 21 | fmptd 6529 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ) |
23 | | mbflimsup.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) |
24 | 23 | ltpnfd 12159 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) < +∞) |
25 | 2, 3 | limsupgre 14419 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ ∧ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) < +∞) → 𝐻:ℝ⟶ℝ) |
26 | 18, 22, 24, 25 | syl3anc 1476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻:ℝ⟶ℝ) |
27 | 26 | frnd 6191 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐻 ⊆ ℝ) |
28 | 17, 27 | syl5ss 3763 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) ⊆ ℝ) |
29 | 26 | fdmd 6193 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐻 = ℝ) |
30 | 29 | ineq1d 3964 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) = (ℝ ∩ 𝑍)) |
31 | | sseqin2 3968 |
. . . . . . . . . 10
⊢ (𝑍 ⊆ ℝ ↔ (ℝ
∩ 𝑍) = 𝑍) |
32 | 10, 31 | mpbi 220 |
. . . . . . . . 9
⊢ (ℝ
∩ 𝑍) = 𝑍 |
33 | 30, 32 | syl6eq 2821 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) = 𝑍) |
34 | | uzid 11907 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
35 | 12, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
36 | 35, 3 | syl6eleqr 2861 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
37 | 36 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ 𝑍) |
38 | 37 | ne0d 4070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ≠ ∅) |
39 | 33, 38 | eqnetrd 3010 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) ≠ ∅) |
40 | | imadisj 5624 |
. . . . . . . 8
⊢ ((𝐻 “ 𝑍) = ∅ ↔ (dom 𝐻 ∩ 𝑍) = ∅) |
41 | 40 | necon3bii 2995 |
. . . . . . 7
⊢ ((𝐻 “ 𝑍) ≠ ∅ ↔ (dom 𝐻 ∩ 𝑍) ≠ ∅) |
42 | 39, 41 | sylibr 224 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) ≠ ∅) |
43 | 23 | leidd 10799 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) |
44 | 20 | rexrd 10294 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈
ℝ*) |
45 | 44, 21 | fmptd 6529 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) |
46 | 23 | rexrd 10294 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈
ℝ*) |
47 | 2 | limsuple 14416 |
. . . . . . . . . . 11
⊢ ((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ* ∧ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ*) → ((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
48 | 11, 45, 46, 47 | syl3anc 1476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
49 | 43, 48 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦)) |
50 | | ssralv 3815 |
. . . . . . . . 9
⊢ (𝑍 ⊆ ℝ →
(∀𝑦 ∈ ℝ
(lim sup‘(𝑛 ∈
𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦) → ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
51 | 10, 49, 50 | mpsyl 68 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦)) |
52 | 2 | limsupgf 14413 |
. . . . . . . . . 10
⊢ 𝐻:ℝ⟶ℝ* |
53 | | ffn 6184 |
. . . . . . . . . 10
⊢ (𝐻:ℝ⟶ℝ* →
𝐻 Fn
ℝ) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝐻 Fn ℝ |
55 | | breq2 4791 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐻‘𝑦) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
56 | 55 | ralima 6643 |
. . . . . . . . 9
⊢ ((𝐻 Fn ℝ ∧ 𝑍 ⊆ ℝ) →
(∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
57 | 54, 11, 56 | sylancr 575 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
58 | 51, 57 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧) |
59 | | breq1 4790 |
. . . . . . . . 9
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (𝑦 ≤ 𝑧 ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧)) |
60 | 59 | ralbidv 3135 |
. . . . . . . 8
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧 ↔ ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧)) |
61 | 60 | rspcev 3460 |
. . . . . . 7
⊢ (((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ ∧ ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) |
62 | 23, 58, 61 | syl2anc 573 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) |
63 | | infxrre 12370 |
. . . . . 6
⊢ (((𝐻 “ 𝑍) ⊆ ℝ ∧ (𝐻 “ 𝑍) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) → inf((𝐻 “ 𝑍), ℝ*, < ) = inf((𝐻 “ 𝑍), ℝ, < )) |
64 | 28, 42, 62, 63 | syl3anc 1476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → inf((𝐻 “ 𝑍), ℝ*, < ) = inf((𝐻 “ 𝑍), ℝ, < )) |
65 | | df-ima 5263 |
. . . . . . 7
⊢ (𝐻 “ 𝑍) = ran (𝐻 ↾ 𝑍) |
66 | 26 | feqmptd 6393 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 = (𝑖 ∈ ℝ ↦ (𝐻‘𝑖))) |
67 | 66 | reseq1d 5532 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍)) |
68 | | resmpt 5589 |
. . . . . . . . . . 11
⊢ (𝑍 ⊆ ℝ → ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖))) |
69 | 10, 68 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖)) |
70 | 67, 69 | syl6eq 2821 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖))) |
71 | 10 | sseli 3748 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ ℝ) |
72 | | ffvelrn 6502 |
. . . . . . . . . . . . 13
⊢ ((𝐻:ℝ⟶ℝ ∧
𝑖 ∈ ℝ) →
(𝐻‘𝑖) ∈ ℝ) |
73 | 26, 71, 72 | syl2an 583 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ∈ ℝ) |
74 | 73 | rexrd 10294 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ∈
ℝ*) |
75 | | simplll 758 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
76 | 3 | uztrn2 11910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
77 | 76 | adantll 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
78 | | simpllr 760 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ 𝐴) |
79 | 75, 77, 78, 19 | syl12anc 1474 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝐵 ∈ ℝ) |
80 | | eqid 2771 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) = (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) |
81 | 79, 80 | fmptd 6529 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ) |
82 | 81 | frnd 6191 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
83 | 80, 79 | dmmptd 6163 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → dom (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) = (ℤ≥‘𝑖)) |
84 | | simpr 471 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
85 | 84, 3 | syl6eleq 2860 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
86 | | eluzelz 11902 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑖 ∈ ℤ) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
88 | 87 | adantlr 694 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
89 | | uzid 11907 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
(ℤ≥‘𝑖)) |
90 | | ne0i 4069 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈
(ℤ≥‘𝑖) → (ℤ≥‘𝑖) ≠ ∅) |
91 | 88, 89, 90 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ≠ ∅) |
92 | 83, 91 | eqnetrd 3010 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → dom (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
93 | | dm0rn0 5479 |
. . . . . . . . . . . . . . 15
⊢ (dom
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) = ∅ ↔ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) = ∅) |
94 | 93 | necon3bii 2995 |
. . . . . . . . . . . . . 14
⊢ (dom
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ↔ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
95 | 92, 94 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
96 | 85 | adantlr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
97 | | uzss 11913 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
99 | 98, 3 | syl6sseqr 3801 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ⊆ 𝑍) |
100 | 73 | leidd 10799 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ≤ (𝐻‘𝑖)) |
101 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑍 ⊆ ℝ) |
102 | 45 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) |
103 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
104 | 10, 103 | sseldi 3750 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℝ) |
105 | 2 | limsupgle 14415 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ (𝐻‘𝑖) ∈ ℝ*) → ((𝐻‘𝑖) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
106 | 101, 102,
104, 74, 105 | syl211anc 1482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((𝐻‘𝑖) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
107 | 100, 106 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
108 | | ssralv 3815 |
. . . . . . . . . . . . . . . . 17
⊢
((ℤ≥‘𝑖) ⊆ 𝑍 → (∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)) → ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
109 | 99, 107, 108 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
110 | 99 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) →
(ℤ≥‘𝑖) ⊆ 𝑍) |
111 | 110 | resmptd 5592 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖)) = (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
112 | 111 | fveq1d 6335 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘)) |
113 | | fvres 6350 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(ℤ≥‘𝑖) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
114 | 113 | adantl 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
115 | 112, 114 | eqtr3d 2807 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
116 | 115 | breq1d 4797 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
117 | | eluzle 11905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈
(ℤ≥‘𝑖) → 𝑖 ≤ 𝑘) |
118 | 117 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → 𝑖 ≤ 𝑘) |
119 | | biimt 349 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ≤ 𝑘 → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
121 | 116, 120 | bitrd 268 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
122 | 121 | ralbidva 3134 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
123 | 109, 122 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)) |
124 | | ffn 6184 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ → (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖)) |
125 | | breq1 4790 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) → (𝑧 ≤ (𝐻‘𝑖) ↔ ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
126 | 125 | ralrn 6507 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
127 | 81, 124, 126 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
128 | 123, 127 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖)) |
129 | | breq2 4791 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝐻‘𝑖) → (𝑧 ≤ 𝑦 ↔ 𝑧 ≤ (𝐻‘𝑖))) |
130 | 129 | ralbidv 3135 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐻‘𝑖) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
131 | 130 | rspcev 3460 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑖) ∈ ℝ ∧ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
132 | 73, 128, 131 | syl2anc 573 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
133 | | suprcl 11188 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
134 | 82, 95, 132, 133 | syl3anc 1476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
135 | 134 | rexrd 10294 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ*) |
136 | 82 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
137 | 95 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
138 | 132 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
139 | 8 | sseli 3748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
140 | | eluz 11906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈
(ℤ≥‘𝑖) ↔ 𝑖 ≤ 𝑘)) |
141 | 88, 139, 140 | syl2an 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑘 ∈ (ℤ≥‘𝑖) ↔ 𝑖 ≤ 𝑘)) |
142 | 141 | biimprd 238 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑖 ≤ 𝑘 → 𝑘 ∈ (ℤ≥‘𝑖))) |
143 | 142 | impr 442 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → 𝑘 ∈ (ℤ≥‘𝑖)) |
144 | 143, 115 | syldan 579 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
145 | 81 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ) |
146 | 145, 124 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖)) |
147 | | fnfvelrn 6501 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
148 | 146, 143,
147 | syl2anc 573 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
149 | 144, 148 | eqeltrrd 2851 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
150 | | suprub 11189 |
. . . . . . . . . . . . . . 15
⊢ (((ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) ∧ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
151 | 136, 137,
138, 149, 150 | syl31anc 1479 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
152 | 151 | expr 444 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
153 | 152 | ralrimiva 3115 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
154 | 2 | limsupgle 14415 |
. . . . . . . . . . . . 13
⊢ (((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ sup(ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ*) → ((𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )))) |
155 | 101, 102,
104, 135, 154 | syl211anc 1482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )))) |
156 | 153, 155 | mpbird 247 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
157 | | suprleub 11194 |
. . . . . . . . . . . . 13
⊢ (((ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) ∧ (𝐻‘𝑖) ∈ ℝ) → (sup(ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
158 | 82, 95, 132, 73, 157 | syl31anc 1479 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
159 | 128, 158 | mpbird 247 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖)) |
160 | 74, 135, 156, 159 | xrletrid 12190 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) = sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
161 | 160 | mpteq2dva 4879 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖)) = (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
162 | 70, 161 | eqtrd 2805 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
163 | 162 | rneqd 5490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝐻 ↾ 𝑍) = ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
164 | 65, 163 | syl5eq 2817 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) = ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
165 | 164 | infeq1d 8542 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → inf((𝐻 “ 𝑍), ℝ, < ) = inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
166 | 16, 64, 165 | 3eqtrd 2809 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) = inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
167 | 166 | mpteq2dva 4879 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
))) |
168 | 1, 167 | syl5eq 2817 |
. 2
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
))) |
169 | | eqid 2771 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) =
(𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
170 | | eqid 2771 |
. . . 4
⊢
(ℤ≥‘𝑖) = (ℤ≥‘𝑖) |
171 | | eqid 2771 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
172 | | simpll 750 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
173 | 76 | adantll 693 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
174 | | mbflimsup.5 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
175 | 172, 173,
174 | syl2anc 573 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
176 | | simpll 750 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝜑) |
177 | 76 | ad2ant2lr 742 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝑛 ∈ 𝑍) |
178 | | simprr 756 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
179 | 176, 177,
178, 19 | syl12anc 1474 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑛 ∈ (ℤ≥‘𝑖) ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
180 | 79 | ralrimiva 3115 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ∈ ℝ) |
181 | | breq1 4790 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → (𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
182 | 80, 181 | ralrnmpt 6513 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(ℤ≥‘𝑖)𝐵 ∈ ℝ → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
183 | 180, 182 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
184 | 183 | rexbidv 3200 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
185 | 132, 184 | mpbid 222 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦) |
186 | 185 | an32s 631 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦) |
187 | 170, 171,
87, 175, 179, 186 | mbfsup 23650 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) ∈
MblFn) |
188 | 134 | an32s 631 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
189 | 188 | anasss 452 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
190 | 2 | limsuple 14416 |
. . . . . . . 8
⊢ ((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ* ∧ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ*) → ((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
191 | 11, 45, 46, 190 | syl3anc 1476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ↔ ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
192 | 43, 191 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖)) |
193 | | ssralv 3815 |
. . . . . 6
⊢ (𝑍 ⊆ ℝ →
(∀𝑖 ∈ ℝ
(lim sup‘(𝑛 ∈
𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
194 | 10, 192, 193 | mpsyl 68 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖)) |
195 | 160 | breq2d 4799 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
196 | 195 | ralbidva 3134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) ↔ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
197 | 194, 196 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
198 | | breq1 4790 |
. . . . . 6
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
199 | 198 | ralbidv 3135 |
. . . . 5
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
200 | 199 | rspcev 3460 |
. . . 4
⊢ (((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ ∧ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) → ∃𝑦 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
201 | 23, 197, 200 | syl2anc 573 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
202 | 3, 169, 12, 187, 189, 201 | mbfinf 23651 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) ∈
MblFn) |
203 | 168, 202 | eqeltrd 2850 |
1
⊢ (𝜑 → 𝐺 ∈ MblFn) |