| Step | Hyp | Ref
| Expression |
| 1 | | mbflimsup.2 |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) |
| 2 | | mbflimsup.h |
. . . . . 6
⊢ 𝐻 = (𝑚 ∈ ℝ ↦ sup((((𝑛 ∈ 𝑍 ↦ 𝐵) “ (𝑚[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 3 | | mbflimsup.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 4 | 3 | fvexi 6920 |
. . . . . . . 8
⊢ 𝑍 ∈ V |
| 5 | 4 | mptex 7243 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V |
| 6 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V) |
| 7 | | uzssz 12899 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 8 | 3, 7 | eqsstri 4030 |
. . . . . . . 8
⊢ 𝑍 ⊆
ℤ |
| 9 | | zssre 12620 |
. . . . . . . 8
⊢ ℤ
⊆ ℝ |
| 10 | 8, 9 | sstri 3993 |
. . . . . . 7
⊢ 𝑍 ⊆
ℝ |
| 11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ⊆ ℝ) |
| 12 | | mbflimsup.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 13 | 3 | uzsup 13903 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) =
+∞) |
| 14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(𝑍, ℝ*, < ) =
+∞) |
| 15 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(𝑍, ℝ*, < ) =
+∞) |
| 16 | 2, 6, 11, 15 | limsupval2 15516 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) = inf((𝐻 “ 𝑍), ℝ*, <
)) |
| 17 | | imassrn 6089 |
. . . . . . 7
⊢ (𝐻 “ 𝑍) ⊆ ran 𝐻 |
| 18 | 12 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ ℤ) |
| 19 | | mbflimsup.6 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
| 20 | 19 | anass1rs 655 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℝ) |
| 21 | 20 | fmpttd 7135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ) |
| 22 | | mbflimsup.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) |
| 23 | 22 | ltpnfd 13163 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) < +∞) |
| 24 | 2, 3 | limsupgre 15517 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ ∧ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) < +∞) → 𝐻:ℝ⟶ℝ) |
| 25 | 18, 21, 23, 24 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻:ℝ⟶ℝ) |
| 26 | 25 | frnd 6744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐻 ⊆ ℝ) |
| 27 | 17, 26 | sstrid 3995 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) ⊆ ℝ) |
| 28 | 25 | fdmd 6746 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐻 = ℝ) |
| 29 | 28 | ineq1d 4219 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) = (ℝ ∩ 𝑍)) |
| 30 | | sseqin2 4223 |
. . . . . . . . . 10
⊢ (𝑍 ⊆ ℝ ↔ (ℝ
∩ 𝑍) = 𝑍) |
| 31 | 10, 30 | mpbi 230 |
. . . . . . . . 9
⊢ (ℝ
∩ 𝑍) = 𝑍 |
| 32 | 29, 31 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) = 𝑍) |
| 33 | | uzid 12893 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
| 34 | 12, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
| 35 | 34, 3 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
| 36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ 𝑍) |
| 37 | 36 | ne0d 4342 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ≠ ∅) |
| 38 | 32, 37 | eqnetrd 3008 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (dom 𝐻 ∩ 𝑍) ≠ ∅) |
| 39 | | imadisj 6098 |
. . . . . . . 8
⊢ ((𝐻 “ 𝑍) = ∅ ↔ (dom 𝐻 ∩ 𝑍) = ∅) |
| 40 | 39 | necon3bii 2993 |
. . . . . . 7
⊢ ((𝐻 “ 𝑍) ≠ ∅ ↔ (dom 𝐻 ∩ 𝑍) ≠ ∅) |
| 41 | 38, 40 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) ≠ ∅) |
| 42 | 22 | leidd 11829 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) |
| 43 | 20 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈
ℝ*) |
| 44 | 43 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) |
| 45 | 22 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈
ℝ*) |
| 46 | 2 | limsuple 15514 |
. . . . . . . . . . 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 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦)) |
| 49 | | ssralv 4052 |
. . . . . . . . 9
⊢ (𝑍 ⊆ ℝ →
(∀𝑦 ∈ ℝ
(lim sup‘(𝑛 ∈
𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦) → ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
| 50 | 10, 48, 49 | mpsyl 68 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦)) |
| 51 | 2 | limsupgf 15511 |
. . . . . . . . . 10
⊢ 𝐻:ℝ⟶ℝ* |
| 52 | | ffn 6736 |
. . . . . . . . . 10
⊢ (𝐻:ℝ⟶ℝ* →
𝐻 Fn
ℝ) |
| 53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝐻 Fn ℝ |
| 54 | | breq2 5147 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐻‘𝑦) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
| 55 | 54 | ralima 7257 |
. . . . . . . . 9
⊢ ((𝐻 Fn ℝ ∧ 𝑍 ⊆ ℝ) →
(∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
| 56 | 53, 11, 55 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑦))) |
| 57 | 50, 56 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧) |
| 58 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (𝑦 ≤ 𝑧 ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧)) |
| 59 | 58 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧 ↔ ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧)) |
| 60 | 59 | rspcev 3622 |
. . . . . . 7
⊢ (((lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ ∧ ∀𝑧 ∈ (𝐻 “ 𝑍)(lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) |
| 61 | 22, 57, 60 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) |
| 62 | | infxrre 13378 |
. . . . . 6
⊢ (((𝐻 “ 𝑍) ⊆ ℝ ∧ (𝐻 “ 𝑍) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻 “ 𝑍)𝑦 ≤ 𝑧) → inf((𝐻 “ 𝑍), ℝ*, < ) = inf((𝐻 “ 𝑍), ℝ, < )) |
| 63 | 27, 41, 61, 62 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → inf((𝐻 “ 𝑍), ℝ*, < ) = inf((𝐻 “ 𝑍), ℝ, < )) |
| 64 | | df-ima 5698 |
. . . . . . 7
⊢ (𝐻 “ 𝑍) = ran (𝐻 ↾ 𝑍) |
| 65 | 25 | feqmptd 6977 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 = (𝑖 ∈ ℝ ↦ (𝐻‘𝑖))) |
| 66 | 65 | reseq1d 5996 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍)) |
| 67 | | resmpt 6055 |
. . . . . . . . . . 11
⊢ (𝑍 ⊆ ℝ → ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖))) |
| 68 | 10, 67 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℝ ↦ (𝐻‘𝑖)) ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖)) |
| 69 | 66, 68 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖))) |
| 70 | 10 | sseli 3979 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ ℝ) |
| 71 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝐻:ℝ⟶ℝ ∧
𝑖 ∈ ℝ) →
(𝐻‘𝑖) ∈ ℝ) |
| 72 | 25, 70, 71 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ∈ ℝ) |
| 73 | 72 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ∈
ℝ*) |
| 74 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
| 75 | 3 | uztrn2 12897 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
| 76 | 75 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ 𝑍) |
| 77 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ 𝐴) |
| 78 | 74, 76, 77, 19 | syl12anc 837 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝐵 ∈ ℝ) |
| 79 | 78 | fmpttd 7135 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ) |
| 80 | 79 | frnd 6744 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
| 81 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) = (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) |
| 82 | 81, 78 | dmmptd 6713 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → dom (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) = (ℤ≥‘𝑖)) |
| 83 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
| 84 | 83, 3 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
| 85 | | eluzelz 12888 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑖 ∈ ℤ) |
| 86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
| 87 | 86 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
| 88 | | uzid 12893 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
(ℤ≥‘𝑖)) |
| 89 | | ne0i 4341 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈
(ℤ≥‘𝑖) → (ℤ≥‘𝑖) ≠ ∅) |
| 90 | 87, 88, 89 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ≠ ∅) |
| 91 | 82, 90 | eqnetrd 3008 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → dom (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
| 92 | | dm0rn0 5935 |
. . . . . . . . . . . . . . 15
⊢ (dom
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) = ∅ ↔ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) = ∅) |
| 93 | 92 | necon3bii 2993 |
. . . . . . . . . . . . . 14
⊢ (dom
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ↔ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
| 94 | 91, 93 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
| 95 | 84 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
| 96 | | uzss 12901 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
| 97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
| 98 | 97, 3 | sseqtrrdi 4025 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (ℤ≥‘𝑖) ⊆ 𝑍) |
| 99 | 72 | leidd 11829 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ≤ (𝐻‘𝑖)) |
| 100 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑍 ⊆ ℝ) |
| 101 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) |
| 102 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
| 103 | 10, 102 | sselid 3981 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℝ) |
| 104 | 2 | limsupgle 15513 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ (𝐻‘𝑖) ∈ ℝ*) → ((𝐻‘𝑖) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
| 105 | 100, 101,
103, 73, 104 | syl211anc 1378 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((𝐻‘𝑖) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
| 106 | 99, 105 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
| 107 | | ssralv 4052 |
. . . . . . . . . . . . . . . . 17
⊢
((ℤ≥‘𝑖) ⊆ 𝑍 → (∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)) → ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
| 108 | 98, 106, 107 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
| 109 | 98 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) →
(ℤ≥‘𝑖) ⊆ 𝑍) |
| 110 | 109 | resmptd 6058 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖)) = (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
| 111 | 110 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘)) |
| 112 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(ℤ≥‘𝑖) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
| 113 | 112 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵) ↾
(ℤ≥‘𝑖))‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
| 114 | 111, 113 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
| 115 | 114 | breq1d 5153 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
| 116 | | eluzle 12891 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈
(ℤ≥‘𝑖) → 𝑖 ≤ 𝑘) |
| 117 | 116 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → 𝑖 ≤ 𝑘) |
| 118 | | biimt 360 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ≤ 𝑘 → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
| 119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
| 120 | 115, 119 | bitrd 279 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
| 121 | 120 | ralbidva 3176 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)(𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)))) |
| 122 | 108, 121 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖)) |
| 123 | | ffn 6736 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ → (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖)) |
| 124 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) → (𝑧 ≤ (𝐻‘𝑖) ↔ ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
| 125 | 124 | ralrn 7108 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
| 126 | 79, 123, 125 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖) ↔ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻‘𝑖))) |
| 127 | 122, 126 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖)) |
| 128 | | brralrspcev 5203 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑖) ∈ ℝ ∧ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
| 129 | 72, 127, 128 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
| 130 | 80, 94, 129 | suprcld 12231 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
| 131 | 130 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ*) |
| 132 | 80 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ) |
| 133 | 94 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅) |
| 134 | 129 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) |
| 135 | 8 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
| 136 | | eluz 12892 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈
(ℤ≥‘𝑖) ↔ 𝑖 ≤ 𝑘)) |
| 137 | 87, 135, 136 | syl2an 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑘 ∈ (ℤ≥‘𝑖) ↔ 𝑖 ≤ 𝑘)) |
| 138 | 137 | biimprd 248 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑖 ≤ 𝑘 → 𝑘 ∈ (ℤ≥‘𝑖))) |
| 139 | 138 | impr 454 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → 𝑘 ∈ (ℤ≥‘𝑖)) |
| 140 | 139, 114 | syldan 591 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
| 141 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵):(ℤ≥‘𝑖)⟶ℝ) |
| 142 | 141, 123 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖)) |
| 143 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) Fn (ℤ≥‘𝑖) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
| 144 | 142, 139,
143 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
| 145 | 140, 144 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)) |
| 146 | 132, 133,
134, 145 | suprubd 12230 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ (𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
| 147 | 146 | expr 456 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
| 148 | 147 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
| 149 | 2 | limsupgle 15513 |
. . . . . . . . . . . . 13
⊢ (((𝑍 ⊆ ℝ ∧ (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ sup(ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ*) → ((𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )))) |
| 150 | 100, 101,
103, 131, 149 | syl211anc 1378 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘 ∈ 𝑍 (𝑖 ≤ 𝑘 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )))) |
| 151 | 148, 150 | mpbird 257 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
| 152 | | suprleub 12234 |
. . . . . . . . . . . . 13
⊢ (((ran
(𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦) ∧ (𝐻‘𝑖) ∈ ℝ) → (sup(ran (𝑛 ∈
(ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
| 153 | 80, 94, 129, 72, 152 | syl31anc 1375 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ (𝐻‘𝑖))) |
| 154 | 127, 153 | mpbird 257 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻‘𝑖)) |
| 155 | 73, 131, 151, 154 | xrletrid 13197 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (𝐻‘𝑖) = sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
| 156 | 155 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑖 ∈ 𝑍 ↦ (𝐻‘𝑖)) = (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
| 157 | 69, 156 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 ↾ 𝑍) = (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
| 158 | 157 | rneqd 5949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝐻 ↾ 𝑍) = ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
| 159 | 64, 158 | eqtrid 2789 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻 “ 𝑍) = ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
| 160 | 159 | infeq1d 9517 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → inf((𝐻 “ 𝑍), ℝ, < ) = inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
| 161 | 16, 63, 160 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) = inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
)) |
| 162 | 161 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, <
))) |
| 163 | 1, 162 | eqtrid 2789 |
. 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 584 |
. . . 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 3146 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ∈ ℝ) |
| 176 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → (𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
| 177 | 81, 176 | ralrnmptw 7114 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(ℤ≥‘𝑖)𝐵 ∈ ℝ → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
| 178 | 175, 177 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
| 179 | 178 | rexbidv 3179 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦)) |
| 180 | 129, 179 | mpbid 232 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦) |
| 181 | 180 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ≥‘𝑖)𝐵 ≤ 𝑦) |
| 182 | 165, 166,
86, 170, 174, 181 | mbfsup 25699 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) ∈
MblFn) |
| 183 | 130 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
| 184 | 183 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
| 185 | 2 | limsuple 15514 |
. . . . . . . 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 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ ℝ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖)) |
| 188 | | ssralv 4052 |
. . . . . 6
⊢ (𝑍 ⊆ ℝ →
(∀𝑖 ∈ ℝ
(lim sup‘(𝑛 ∈
𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖))) |
| 189 | 10, 187, 188 | mpsyl 68 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖)) |
| 190 | 155 | breq2d 5155 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝑍) → ((lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) ↔ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
| 191 | 190 | ralbidva 3176 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ (𝐻‘𝑖) ↔ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
| 192 | 189, 191 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )) |
| 193 | | breq1 5146 |
. . . . . 6
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ (lim
sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
| 194 | 193 | ralbidv 3178 |
. . . . 5
⊢ (𝑦 = (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) → (∀𝑖 ∈ 𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑖 ∈ 𝑍 (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < ))) |
| 195 | 194 | rspcev 3622 |
. . . 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 25700 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ inf(ran (𝑖 ∈ 𝑍 ↦ sup(ran (𝑛 ∈ (ℤ≥‘𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) ∈
MblFn) |
| 198 | 163, 197 | eqeltrd 2841 |
1
⊢ (𝜑 → 𝐺 ∈ MblFn) |