| Step | Hyp | Ref
| Expression |
| 1 | | sge0reuz.k |
. . 3
⊢
Ⅎ𝑘𝜑 |
| 2 | | sge0reuz.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑍 = (ℤ≥‘𝑀)) |
| 4 | | fvex 6919 |
. . . 4
⊢
(ℤ≥‘𝑀) ∈ V |
| 5 | 3, 4 | eqeltrdi 2849 |
. . 3
⊢ (𝜑 → 𝑍 ∈ V) |
| 6 | | sge0reuz.b |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ (0[,)+∞)) |
| 7 | 1, 5, 6 | sge0revalmpt 46393 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵), ℝ*, <
)) |
| 8 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
| 9 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵) = (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵) |
| 10 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑥 ∈ (𝒫 𝑍 ∩ Fin) |
| 11 | 1, 10 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin)) |
| 12 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝑍 ∩ Fin) → 𝑥 ∈ Fin) |
| 13 | 12 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑥 ∈ Fin) |
| 14 | | rge0ssre 13496 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
| 15 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝜑) |
| 16 | | elpwinss 45054 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝒫 𝑍 ∩ Fin) → 𝑥 ⊆ 𝑍) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘 ∈ 𝑥) → 𝑥 ⊆ 𝑍) |
| 18 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝑥) |
| 19 | 17, 18 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝑍) |
| 20 | 19 | adantll 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝑍) |
| 21 | 15, 20, 6 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐵 ∈ (0[,)+∞)) |
| 22 | 14, 21 | sselid 3981 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐵 ∈ ℝ) |
| 23 | 11, 13, 22 | fsumreclf 45591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑘 ∈ 𝑥 𝐵 ∈ ℝ) |
| 24 | 23 | rexrd 11311 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑘 ∈ 𝑥 𝐵 ∈
ℝ*) |
| 25 | 8, 9, 24 | rnmptssd 45201 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵) ⊆
ℝ*) |
| 26 | | supxrcl 13357 |
. . . 4
⊢ (ran
(𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵) ⊆ ℝ* → sup(ran
(𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵), ℝ*, < ) ∈
ℝ*) |
| 27 | 25, 26 | syl 17 |
. . 3
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵), ℝ*, < ) ∈
ℝ*) |
| 28 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑛𝜑 |
| 29 | | eqid 2737 |
. . . . 5
⊢ (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) = (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 30 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑛 ∈ 𝑍 |
| 31 | 1, 30 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑛 ∈ 𝑍) |
| 32 | | fzfid 14014 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀...𝑛) ∈ Fin) |
| 33 | | elfzuz 13560 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑀...𝑛) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 34 | 33, 2 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀...𝑛) → 𝑘 ∈ 𝑍) |
| 35 | 34 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑘 ∈ 𝑍) |
| 36 | 14, 6 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ) |
| 37 | 35, 36 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝐵 ∈ ℝ) |
| 38 | 37 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝐵 ∈ ℝ) |
| 39 | 31, 32, 38 | fsumreclf 45591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑛)𝐵 ∈ ℝ) |
| 40 | 39 | rexrd 11311 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑛)𝐵 ∈
ℝ*) |
| 41 | 28, 29, 40 | rnmptssd 45201 |
. . . 4
⊢ (𝜑 → ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) ⊆
ℝ*) |
| 42 | | supxrcl 13357 |
. . . 4
⊢ (ran
(𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) ⊆ ℝ* → sup(ran
(𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ*, < ) ∈
ℝ*) |
| 43 | 41, 42 | syl 17 |
. . 3
⊢ (𝜑 → sup(ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ*, < ) ∈
ℝ*) |
| 44 | | vex 3484 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
| 45 | 9 | elrnmpt 5969 |
. . . . . . . 8
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵) ↔ ∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑥 𝐵)) |
| 46 | 44, 45 | ax-mp 5 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵) ↔ ∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑥 𝐵) |
| 47 | 46 | biimpi 216 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵) → ∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑥 𝐵) |
| 48 | 47 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵)) → ∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑥 𝐵) |
| 49 | | sge0reuz.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 50 | 49 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) → 𝑀 ∈ ℤ) |
| 51 | 16 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) → 𝑥 ⊆ 𝑍) |
| 52 | 13 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) → 𝑥 ∈ Fin) |
| 53 | 50, 2, 51, 52 | uzfissfz 45337 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) → ∃𝑛 ∈ 𝑍 𝑥 ⊆ (𝑀...𝑛)) |
| 54 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) |
| 55 | | nfmpt1 5250 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 56 | 55 | nfrn 5963 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛ran
(𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 57 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑦 ≤ 𝑤 |
| 58 | 56, 57 | nfrexw 3313 |
. . . . . . . . . 10
⊢
Ⅎ𝑛∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤 |
| 59 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) |
| 60 | | sumex 15724 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑘 ∈
(𝑀...𝑛)𝐵 ∈ V |
| 61 | 60 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝑍 → Σ𝑘 ∈ (𝑀...𝑛)𝐵 ∈ V) |
| 62 | 29 | elrnmpt1 5971 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝑛)𝐵 ∈ V) → Σ𝑘 ∈ (𝑀...𝑛)𝐵 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)) |
| 63 | 59, 61, 62 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → Σ𝑘 ∈ (𝑀...𝑛)𝐵 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)) |
| 64 | 63 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ⊆ (𝑀...𝑛)) → Σ𝑘 ∈ (𝑀...𝑛)𝐵 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)) |
| 65 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝑀...𝑛)) → 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) |
| 66 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘𝑦 |
| 67 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑘𝑥 |
| 68 | 67 | nfsum1 15726 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘Σ𝑘 ∈ 𝑥 𝐵 |
| 69 | 66, 68 | nfeq 2919 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘 𝑦 = Σ𝑘 ∈ 𝑥 𝐵 |
| 70 | 1, 69 | nfan 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘(𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) |
| 71 | | nfv 1914 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘 𝑥 ⊆ (𝑀...𝑛) |
| 72 | 70, 71 | nfan 1899 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝑀...𝑛)) |
| 73 | | fzfid 14014 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝑀...𝑛)) → (𝑀...𝑛) ∈ Fin) |
| 74 | 37 | ad4ant14 752 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝑀...𝑛)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝐵 ∈ ℝ) |
| 75 | | simplll 775 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝑀...𝑛)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝜑) |
| 76 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝑀...𝑛)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑘 ∈ 𝑍) |
| 77 | | 0xr 11308 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ* |
| 78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ∈
ℝ*) |
| 79 | | pnfxr 11315 |
. . . . . . . . . . . . . . . . . . 19
⊢ +∞
∈ ℝ* |
| 80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → +∞ ∈
ℝ*) |
| 81 | | icogelb 13438 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐵 ∈ (0[,)+∞))
→ 0 ≤ 𝐵) |
| 82 | 78, 80, 6, 81 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐵) |
| 83 | 75, 76, 82 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝑀...𝑛)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 0 ≤ 𝐵) |
| 84 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝑀...𝑛)) → 𝑥 ⊆ (𝑀...𝑛)) |
| 85 | 72, 73, 74, 83, 84 | fsumlessf 45592 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝑀...𝑛)) → Σ𝑘 ∈ 𝑥 𝐵 ≤ Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 86 | 65, 85 | eqbrtrd 5165 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝑀...𝑛)) → 𝑦 ≤ Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 87 | 86 | 3adant2 1132 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ⊆ (𝑀...𝑛)) → 𝑦 ≤ Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 88 | | breq2 5147 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = Σ𝑘 ∈ (𝑀...𝑛)𝐵 → (𝑦 ≤ 𝑤 ↔ 𝑦 ≤ Σ𝑘 ∈ (𝑀...𝑛)𝐵)) |
| 89 | 88 | rspcev 3622 |
. . . . . . . . . . . . 13
⊢
((Σ𝑘 ∈
(𝑀...𝑛)𝐵 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) ∧ 𝑦 ≤ Σ𝑘 ∈ (𝑀...𝑛)𝐵) → ∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤) |
| 90 | 64, 87, 89 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ⊆ (𝑀...𝑛)) → ∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤) |
| 91 | 90 | 3exp 1120 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) → (𝑛 ∈ 𝑍 → (𝑥 ⊆ (𝑀...𝑛) → ∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤))) |
| 92 | 91 | 3adant2 1132 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) → (𝑛 ∈ 𝑍 → (𝑥 ⊆ (𝑀...𝑛) → ∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤))) |
| 93 | 54, 58, 92 | rexlimd 3266 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) → (∃𝑛 ∈ 𝑍 𝑥 ⊆ (𝑀...𝑛) → ∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤)) |
| 94 | 53, 93 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ 𝑥 𝐵) → ∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤) |
| 95 | 94 | 3exp 1120 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝒫 𝑍 ∩ Fin) → (𝑦 = Σ𝑘 ∈ 𝑥 𝐵 → ∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤))) |
| 96 | 95 | rexlimdv 3153 |
. . . . . 6
⊢ (𝜑 → (∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑥 𝐵 → ∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤)) |
| 97 | 96 | imp 406 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑥 𝐵) → ∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤) |
| 98 | 48, 97 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵)) → ∃𝑤 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ≤ 𝑤) |
| 99 | 25, 41, 98 | suplesup2 45387 |
. . 3
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵), ℝ*, < ) ≤ sup(ran
(𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ*, <
)) |
| 100 | 29 | elrnmpt 5969 |
. . . . . . . . . 10
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) ↔ ∃𝑛 ∈ 𝑍 𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵)) |
| 101 | 44, 100 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) ↔ ∃𝑛 ∈ 𝑍 𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 102 | 101 | biimpi 216 |
. . . . . . . 8
⊢ (𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) → ∃𝑛 ∈ 𝑍 𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 103 | 102 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)) → ∃𝑛 ∈ 𝑍 𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 104 | 34 | ssriv 3987 |
. . . . . . . . . . . . . . 15
⊢ (𝑀...𝑛) ⊆ 𝑍 |
| 105 | | ovex 7464 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀...𝑛) ∈ V |
| 106 | 105 | elpw 4604 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀...𝑛) ∈ 𝒫 𝑍 ↔ (𝑀...𝑛) ⊆ 𝑍) |
| 107 | 104, 106 | mpbir 231 |
. . . . . . . . . . . . . 14
⊢ (𝑀...𝑛) ∈ 𝒫 𝑍 |
| 108 | | fzfi 14013 |
. . . . . . . . . . . . . 14
⊢ (𝑀...𝑛) ∈ Fin |
| 109 | 107, 108 | elini 4199 |
. . . . . . . . . . . . 13
⊢ (𝑀...𝑛) ∈ (𝒫 𝑍 ∩ Fin) |
| 110 | 109 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵 → (𝑀...𝑛) ∈ (𝒫 𝑍 ∩ Fin)) |
| 111 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵 → 𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 112 | | sumeq1 15725 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑀...𝑛) → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ (𝑀...𝑛)𝐵) |
| 113 | 112 | rspceeqv 3645 |
. . . . . . . . . . . 12
⊢ (((𝑀...𝑛) ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵) → ∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑥 𝐵) |
| 114 | 110, 111,
113 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵 → ∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑥 𝐵) |
| 115 | 44 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵 → 𝑦 ∈ V) |
| 116 | 9, 114, 115 | elrnmptd 5974 |
. . . . . . . . . 10
⊢ (𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵 → 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵)) |
| 117 | 116 | 2a1i 12 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑍 → (𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵 → 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵)))) |
| 118 | 117 | rexlimdv 3153 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵 → 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵))) |
| 119 | 118 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)) → (∃𝑛 ∈ 𝑍 𝑦 = Σ𝑘 ∈ (𝑀...𝑛)𝐵 → 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵))) |
| 120 | 103, 119 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)) → 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵)) |
| 121 | 120 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵)) |
| 122 | | dfss3 3972 |
. . . . 5
⊢ (ran
(𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵) ↔ ∀𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵)𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵)) |
| 123 | 121, 122 | sylibr 234 |
. . . 4
⊢ (𝜑 → ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵)) |
| 124 | | supxrss 13374 |
. . . 4
⊢ ((ran
(𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵) ∧ ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵) ⊆ ℝ*) →
sup(ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ*, < ) ≤ sup(ran
(𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵), ℝ*, <
)) |
| 125 | 123, 25, 124 | syl2anc 584 |
. . 3
⊢ (𝜑 → sup(ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ*, < ) ≤ sup(ran
(𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵), ℝ*, <
)) |
| 126 | 27, 43, 99, 125 | xrletrid 13197 |
. 2
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑍 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐵), ℝ*, < ) = sup(ran
(𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ*, <
)) |
| 127 | 7, 126 | eqtrd 2777 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐵)) = sup(ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ*, <
)) |