| Step | Hyp | Ref
| Expression |
| 1 | | meaiuninclem.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑁) |
| 2 | | meaiuninclem.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 3 | | 0xr 11308 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
| 4 | 3 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ∈
ℝ*) |
| 5 | | pnfxr 11315 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
| 6 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → +∞ ∈
ℝ*) |
| 7 | | meaiuninclem.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ Meas) |
| 8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas) |
| 9 | | eqid 2737 |
. . . . . . 7
⊢ dom 𝑀 = dom 𝑀 |
| 10 | | meaiuninclem.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) |
| 11 | 10 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀) |
| 12 | 8, 9, 11 | meaxrcl 46476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈
ℝ*) |
| 13 | 8, 11 | meage0 46490 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐸‘𝑛))) |
| 14 | | meaiuninclem.b |
. . . . . . . 8
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 16 | | simp1 1137 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝜑 ∧ 𝑛 ∈ 𝑍)) |
| 17 | | simp2 1138 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ) |
| 18 | | simp3 1139 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 19 | 16 | simprd 495 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑛 ∈ 𝑍) |
| 20 | | rspa 3248 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 21 | 18, 19, 20 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 22 | 12 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ∈
ℝ*) |
| 23 | | rexr 11307 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
| 24 | 23 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ*) |
| 25 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → +∞ ∈
ℝ*) |
| 26 | | simp3 1139 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 27 | | ltpnf 13162 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 < +∞) |
| 28 | 27 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 < +∞) |
| 29 | 22, 24, 25, 26, 28 | xrlelttrd 13202 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞) |
| 30 | 16, 17, 21, 29 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞) |
| 31 | 30 | 3exp 1120 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ ℝ → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞))) |
| 32 | 31 | rexlimdv 3153 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞)) |
| 33 | 15, 32 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) < +∞) |
| 34 | 4, 6, 12, 13, 33 | elicod 13437 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ (0[,)+∞)) |
| 35 | | meaiuninclem.s |
. . . . 5
⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) |
| 36 | 34, 35 | fmptd 7134 |
. . . 4
⊢ (𝜑 → 𝑆:𝑍⟶(0[,)+∞)) |
| 37 | | rge0ssre 13496 |
. . . . 5
⊢
(0[,)+∞) ⊆ ℝ |
| 38 | 37 | a1i 11 |
. . . 4
⊢ (𝜑 → (0[,)+∞) ⊆
ℝ) |
| 39 | 36, 38 | fssd 6753 |
. . 3
⊢ (𝜑 → 𝑆:𝑍⟶ℝ) |
| 40 | 1 | peano2uzs 12944 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍) |
| 41 | 40 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍) |
| 42 | 10 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀) |
| 43 | 41, 42 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀) |
| 44 | | meaiuninclem.i |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) |
| 45 | 8, 9, 11, 43, 44 | meassle 46478 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1)))) |
| 46 | 35 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))) |
| 47 | | fvexd 6921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ V) |
| 48 | 46, 47 | fvmpt2d 7029 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛))) |
| 49 | | 2fveq3 6911 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑚))) |
| 50 | 49 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚))) |
| 51 | 35, 50 | eqtri 2765 |
. . . . . 6
⊢ 𝑆 = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚))) |
| 52 | | 2fveq3 6911 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → (𝑀‘(𝐸‘𝑚)) = (𝑀‘(𝐸‘(𝑛 + 1)))) |
| 53 | | fvexd 6921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘(𝑛 + 1))) ∈ V) |
| 54 | 51, 52, 41, 53 | fvmptd3 7039 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘(𝑛 + 1)) = (𝑀‘(𝐸‘(𝑛 + 1)))) |
| 55 | 48, 54 | breq12d 5156 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)) ↔ (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1))))) |
| 56 | 45, 55 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1))) |
| 57 | 48 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑆‘𝑛)) |
| 58 | 57 | breq1d 5153 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑆‘𝑛) ≤ 𝑥)) |
| 59 | 58 | ralbidva 3176 |
. . . . . . 7
⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
| 60 | 59 | biimpd 229 |
. . . . . 6
⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
| 61 | 60 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
| 62 | 61 | reximdva 3168 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
| 63 | 14, 62 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥) |
| 64 | 1, 2, 39, 56, 63 | climsup 15706 |
. 2
⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < )) |
| 65 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑛𝜑 |
| 66 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
| 67 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) |
| 68 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝐸‘𝑛) ∈ V |
| 69 | 68 | difexi 5330 |
. . . . . . . . . . . 12
⊢ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V |
| 70 | 69 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) |
| 71 | | meaiuninclem.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 72 | 71 | fvmpt2 7027 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 73 | 67, 70, 72 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 74 | 73 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 75 | 7, 9 | dmmeasal 46467 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑀 ∈ SAlg) |
| 76 | 75 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg) |
| 77 | | fzoct 45395 |
. . . . . . . . . . . 12
⊢ (𝑁..^𝑛) ≼ ω |
| 78 | 77 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁..^𝑛) ≼ ω) |
| 79 | 10 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝐸:𝑍⟶dom 𝑀) |
| 80 | | fzossuz 45392 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁..^𝑛) ⊆ (ℤ≥‘𝑁) |
| 81 | 1 | eqcomi 2746 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘𝑁) = 𝑍 |
| 82 | 80, 81 | sseqtri 4032 |
. . . . . . . . . . . . . . 15
⊢ (𝑁..^𝑛) ⊆ 𝑍 |
| 83 | 82 | sseli 3979 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ 𝑍) |
| 84 | 83 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ 𝑍) |
| 85 | 79, 84 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀) |
| 86 | 85 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀) |
| 87 | 76, 78, 86 | saliuncl 46338 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀) |
| 88 | | saldifcl2 46343 |
. . . . . . . . . 10
⊢ ((dom
𝑀 ∈ SAlg ∧ (𝐸‘𝑛) ∈ dom 𝑀 ∧ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀) |
| 89 | 76, 11, 87, 88 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀) |
| 90 | 74, 89 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀) |
| 91 | 8, 9, 90 | meaxrcl 46476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈
ℝ*) |
| 92 | 8, 90 | meage0 46490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐹‘𝑛))) |
| 93 | | difssd 4137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛)) |
| 94 | 74, 93 | eqsstrd 4018 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
| 95 | 8, 9, 90, 11, 94 | meassle 46478 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ≤ (𝑀‘(𝐸‘𝑛))) |
| 96 | 91, 12, 6, 95, 33 | xrlelttrd 13202 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) < +∞) |
| 97 | 4, 6, 91, 92, 96 | elicod 13437 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞)) |
| 98 | | 2fveq3 6911 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑖 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑖))) |
| 99 | 98 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)) |
| 100 | 99 | cbvralvw 3237 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) |
| 101 | 100 | biimpi 216 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) |
| 102 | 101 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) |
| 103 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝑛 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍)) |
| 104 | 103 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑖 ∈ 𝑍))) |
| 105 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑖 → (𝑁...𝑛) = (𝑁...𝑖)) |
| 106 | 105 | sumeq1d 15736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))) |
| 107 | 98, 106 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) ↔ (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))) |
| 108 | 104, 107 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))))) |
| 109 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑍 ↔ 𝑛 ∈ 𝑍)) |
| 110 | 109 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑚 ∈ 𝑍) ↔ (𝜑 ∧ 𝑛 ∈ 𝑍))) |
| 111 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑛 → (𝑁...𝑚) = (𝑁...𝑛)) |
| 112 | 111 | iuneq1d 5019 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
| 113 | 111 | iuneq1d 5019 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → ∪
𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)) |
| 114 | 112, 113 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) ↔ ∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))) |
| 115 | 110, 114 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) ↔ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)))) |
| 116 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑛 → (𝐹‘𝑖) = (𝐹‘𝑛)) |
| 117 | 116 | cbviunv 5040 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) |
| 118 | 117 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) |
| 119 | 65, 1, 10, 71 | iundjiun 46475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))) |
| 120 | 119 | simplld 768 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 121 | 120 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 122 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
| 123 | | rspa 3248 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑚 ∈
𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ 𝑚 ∈ 𝑍) → ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 124 | 121, 122,
123 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 125 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑖 → (𝐸‘𝑛) = (𝐸‘𝑖)) |
| 126 | 125 | cbviunv 5040 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) |
| 127 | 126 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) |
| 128 | 118, 124,
127 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) |
| 129 | 115, 128 | chvarvv 1998 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)) |
| 130 | 67, 1 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑁)) |
| 131 | 130 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ≥‘𝑁)) |
| 132 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑖 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑖 + 1))) |
| 133 | 125, 132 | sseq12d 4017 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑖 → ((𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)) ↔ (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))) |
| 134 | 104, 133 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))))) |
| 135 | 134, 44 | chvarvv 1998 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))) |
| 136 | 84, 135 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))) |
| 137 | 136 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))) |
| 138 | 131, 137 | iunincfi 45099 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖) = (𝐸‘𝑛)) |
| 139 | 129, 138 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
| 140 | 139 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑀‘∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))) |
| 141 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖(𝜑 ∧ 𝑛 ∈ 𝑍) |
| 142 | | elfzuz 13560 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ (ℤ≥‘𝑁)) |
| 143 | 142, 81 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ 𝑍) |
| 144 | 143 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → 𝑖 ∈ 𝑍) |
| 145 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖)) |
| 146 | 145 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑖 → ((𝐹‘𝑛) ∈ dom 𝑀 ↔ (𝐹‘𝑖) ∈ dom 𝑀)) |
| 147 | 104, 146 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀))) |
| 148 | 147, 90 | chvarvv 1998 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀) |
| 149 | 144, 148 | syldan 591 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀) |
| 150 | 149 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀) |
| 151 | | fzct 45390 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁...𝑛) ≼ ω |
| 152 | 151 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ≼ ω) |
| 153 | 144 | ssd 45085 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁...𝑛) ⊆ 𝑍) |
| 154 | 119 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)) |
| 155 | 145 | cbvdisjv 5121 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Disj 𝑛
∈ 𝑍 (𝐹‘𝑛) ↔ Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖)) |
| 156 | 154, 155 | sylib 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖)) |
| 157 | | disjss1 5116 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁...𝑛) ⊆ 𝑍 → (Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))) |
| 158 | 153, 156,
157 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
| 159 | 158 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
| 160 | 141, 8, 9, 150, 152, 159 | meadjiun 46481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) =
(Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖))))) |
| 161 | | fzfid 14014 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ∈ Fin) |
| 162 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑖 → (𝑀‘(𝐹‘𝑛)) = (𝑀‘(𝐹‘𝑖))) |
| 163 | 162 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞) ↔ (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))) |
| 164 | 104, 163 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)))) |
| 165 | 164, 97 | chvarvv 1998 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)) |
| 166 | 144, 165 | syldan 591 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)) |
| 167 | 166 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)) |
| 168 | 161, 167 | sge0fsummpt 46405 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) →
(Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖))) |
| 169 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑚 → (𝑀‘(𝐹‘𝑖)) = (𝑀‘(𝐹‘𝑚))) |
| 170 | 169 | cbvsumv 15732 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ𝑖 ∈
(𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) |
| 171 | 170 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) |
| 172 | 168, 171 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) →
(Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) |
| 173 | 140, 160,
172 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) |
| 174 | 108, 173 | chvarvv 1998 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))) |
| 175 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → (𝑀‘(𝐹‘𝑚)) = (𝑀‘(𝐹‘𝑛))) |
| 176 | 175 | cbvsumv 15732 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑚 ∈
(𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) |
| 177 | 176 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))) |
| 178 | 174, 177 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))) |
| 179 | 178 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
| 180 | 179 | ralbidva 3176 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
| 181 | 180 | biimpd 229 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
| 182 | 181 | imp 406 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥) |
| 183 | 102, 182 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥) |
| 184 | 183 | ex 412 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
| 185 | 184 | reximdv 3170 |
. . . . . . 7
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
| 186 | 14, 185 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥) |
| 187 | 65, 66, 2, 1, 97, 186 | sge0reuzb 46463 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < )) |
| 188 | 98 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) |
| 189 | 35, 188 | eqtri 2765 |
. . . . . . . . 9
⊢ 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) |
| 190 | 189 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))) |
| 191 | 178 | mpteq2dva 5242 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))) |
| 192 | 190, 191 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))) |
| 193 | 192 | rneqd 5949 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 = ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))) |
| 194 | 193 | supeq1d 9486 |
. . . . 5
⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < )) |
| 195 | 187, 194 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran 𝑆, ℝ, < )) |
| 196 | 195 | eqcomd 2743 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) =
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛))))) |
| 197 | 1 | uzct 45068 |
. . . . . 6
⊢ 𝑍 ≼
ω |
| 198 | 197 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑍 ≼ ω) |
| 199 | 65, 7, 9, 90, 198, 154 | meadjiun 46481 |
. . . 4
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛)) =
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛))))) |
| 200 | 199 | eqcomd 2743 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛))) |
| 201 | 119 | simplrd 770 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
| 202 | 201 | fveq2d 6910 |
. . 3
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 203 | 196, 200,
202 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 204 | 64, 203 | breqtrd 5169 |
1
⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |