Step | Hyp | Ref
| Expression |
1 | | meaiuninclem.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑁) |
2 | | meaiuninclem.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
3 | | 0xr 9965 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
4 | 3 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ∈
ℝ*) |
5 | | pnfxr 9971 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
6 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → +∞ ∈
ℝ*) |
7 | | meaiuninclem.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ Meas) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas) |
9 | | eqid 2610 |
. . . . . . 7
⊢ dom 𝑀 = dom 𝑀 |
10 | | meaiuninclem.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) |
11 | 10 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀) |
12 | 8, 9, 11 | meaxrcl 39354 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈
ℝ*) |
13 | 8, 11 | meage0 39368 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐸‘𝑛))) |
14 | | meaiuninclem.b |
. . . . . . . 8
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
16 | | simp1 1054 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝜑 ∧ 𝑛 ∈ 𝑍)) |
17 | | simp2 1055 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ) |
18 | | simp3 1056 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
19 | 16 | simprd 478 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑛 ∈ 𝑍) |
20 | | rspa 2914 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
21 | 18, 19, 20 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
22 | 12 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ∈
ℝ*) |
23 | | rexr 9964 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
24 | 23 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ*) |
25 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → +∞ ∈
ℝ*) |
26 | | simp3 1056 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
27 | | ltpnf 11830 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 < +∞) |
28 | 27 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 < +∞) |
29 | 22, 24, 25, 26, 28 | xrlelttrd 11867 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞) |
30 | 16, 17, 21, 29 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞) |
31 | 30 | 3exp 1256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ ℝ → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞))) |
32 | 31 | rexlimdv 3012 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞)) |
33 | 15, 32 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) < +∞) |
34 | 4, 6, 12, 13, 33 | elicod 12095 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ (0[,)+∞)) |
35 | | meaiuninclem.s |
. . . . 5
⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) |
36 | 34, 35 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝑆:𝑍⟶(0[,)+∞)) |
37 | | rge0ssre 12151 |
. . . . 5
⊢
(0[,)+∞) ⊆ ℝ |
38 | 37 | a1i 11 |
. . . 4
⊢ (𝜑 → (0[,)+∞) ⊆
ℝ) |
39 | 36, 38 | fssd 5970 |
. . 3
⊢ (𝜑 → 𝑆:𝑍⟶ℝ) |
40 | 1 | peano2uzs 11618 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍) |
41 | 40 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍) |
42 | 10 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀) |
43 | 41, 42 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀) |
44 | | meaiuninclem.i |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) |
45 | 8, 9, 11, 43, 44 | meassle 39356 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1)))) |
46 | 35 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))) |
47 | 12 | elexd 3187 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ V) |
48 | 46, 47 | fvmpt2d 6202 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛))) |
49 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚)) |
50 | 49 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑚))) |
51 | 50 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚))) |
52 | 35, 51 | eqtri 2632 |
. . . . . . 7
⊢ 𝑆 = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚))) |
53 | 52 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚)))) |
54 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → (𝐸‘𝑚) = (𝐸‘(𝑛 + 1))) |
55 | 54 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (𝑀‘(𝐸‘𝑚)) = (𝑀‘(𝐸‘(𝑛 + 1)))) |
56 | 55 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 = (𝑛 + 1)) → (𝑀‘(𝐸‘𝑚)) = (𝑀‘(𝐸‘(𝑛 + 1)))) |
57 | | fvex 6113 |
. . . . . . 7
⊢ (𝑀‘(𝐸‘(𝑛 + 1))) ∈ V |
58 | 57 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘(𝑛 + 1))) ∈ V) |
59 | 53, 56, 41, 58 | fvmptd 6197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘(𝑛 + 1)) = (𝑀‘(𝐸‘(𝑛 + 1)))) |
60 | 48, 59 | breq12d 4596 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)) ↔ (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1))))) |
61 | 45, 60 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1))) |
62 | 48 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑆‘𝑛)) |
63 | 62 | breq1d 4593 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑆‘𝑛) ≤ 𝑥)) |
64 | 63 | ralbidva 2968 |
. . . . . . 7
⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
65 | 64 | biimpd 218 |
. . . . . 6
⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
66 | 65 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
67 | 66 | reximdva 3000 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
68 | 14, 67 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥) |
69 | 1, 2, 39, 61, 68 | climsup 14248 |
. 2
⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < )) |
70 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑛𝜑 |
71 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
72 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) |
73 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐸‘𝑛) ∈ V |
74 | 73 | difexi 4736 |
. . . . . . . . . . . 12
⊢ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V |
75 | 74 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) |
76 | | meaiuninclem.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
77 | 76 | fvmpt2 6200 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
78 | 72, 75, 77 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
79 | 78 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
80 | 7, 9 | dmmeasal 39345 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑀 ∈ SAlg) |
81 | 80 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg) |
82 | | fzoct 38544 |
. . . . . . . . . . . 12
⊢ (𝑁..^𝑛) ≼ ω |
83 | 82 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁..^𝑛) ≼ ω) |
84 | 10 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝐸:𝑍⟶dom 𝑀) |
85 | | fzossuz 38539 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁..^𝑛) ⊆ (ℤ≥‘𝑁) |
86 | 1 | eqcomi 2619 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘𝑁) = 𝑍 |
87 | 85, 86 | sseqtri 3600 |
. . . . . . . . . . . . . . 15
⊢ (𝑁..^𝑛) ⊆ 𝑍 |
88 | 87 | sseli 3564 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ 𝑍) |
89 | 88 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ 𝑍) |
90 | 84, 89 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀) |
91 | 90 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀) |
92 | 81, 83, 91 | saliuncl 39218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀) |
93 | | saldifcl2 39222 |
. . . . . . . . . 10
⊢ ((dom
𝑀 ∈ SAlg ∧ (𝐸‘𝑛) ∈ dom 𝑀 ∧ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀) |
94 | 81, 11, 92, 93 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀) |
95 | 79, 94 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀) |
96 | 8, 9, 95 | meaxrcl 39354 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈
ℝ*) |
97 | 8, 95 | meage0 39368 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐹‘𝑛))) |
98 | | difssd 3700 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛)) |
99 | 79, 98 | eqsstrd 3602 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
100 | 8, 9, 95, 11, 99 | meassle 39356 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ≤ (𝑀‘(𝐸‘𝑛))) |
101 | 96, 12, 6, 100, 33 | xrlelttrd 11867 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) < +∞) |
102 | 4, 6, 96, 97, 101 | elicod 12095 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞)) |
103 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑖 → (𝐸‘𝑛) = (𝐸‘𝑖)) |
104 | 103 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑖 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑖))) |
105 | 104 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)) |
106 | 105 | cbvralv 3147 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) |
107 | 106 | biimpi 205 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) |
108 | 107 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) |
109 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝑛 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍)) |
110 | 109 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑖 ∈ 𝑍))) |
111 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑖 → (𝑁...𝑛) = (𝑁...𝑖)) |
112 | 111 | sumeq1d 14279 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))) |
113 | 104, 112 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) ↔ (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))) |
114 | 110, 113 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))))) |
115 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑍 ↔ 𝑛 ∈ 𝑍)) |
116 | 115 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑚 ∈ 𝑍) ↔ (𝜑 ∧ 𝑛 ∈ 𝑍))) |
117 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑛 → (𝑁...𝑚) = (𝑁...𝑛)) |
118 | 117 | iuneq1d 4481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
119 | 117 | iuneq1d 4481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → ∪
𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)) |
120 | 118, 119 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) ↔ ∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))) |
121 | 116, 120 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) ↔ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)))) |
122 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑛 → (𝐹‘𝑖) = (𝐹‘𝑛)) |
123 | 122 | cbviunv 4495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) |
124 | 123 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) |
125 | 70, 1, 10, 76 | iundjiun 39353 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))) |
126 | 125 | simplld 787 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
127 | 126 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
128 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
129 | | rspa 2914 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑚 ∈
𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ 𝑚 ∈ 𝑍) → ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
130 | 127, 128,
129 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
131 | 103 | cbviunv 4495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) |
133 | 124, 130,
132 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) |
134 | 121, 133 | chvarv 2251 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)) |
135 | 72, 1 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑁)) |
136 | 135 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ≥‘𝑁)) |
137 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑖 → (𝑛 + 1) = (𝑖 + 1)) |
138 | 137 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑖 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑖 + 1))) |
139 | 103, 138 | sseq12d 3597 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑖 → ((𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)) ↔ (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))) |
140 | 110, 139 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))))) |
141 | 140, 44 | chvarv 2251 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))) |
142 | 89, 141 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))) |
143 | 142 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))) |
144 | 136, 143 | iunincfi 38300 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖) = (𝐸‘𝑛)) |
145 | 134, 144 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
146 | 145 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑀‘∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))) |
147 | | nfv 1830 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖(𝜑 ∧ 𝑛 ∈ 𝑍) |
148 | | elfzuz 12209 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ (ℤ≥‘𝑁)) |
149 | 148, 86 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ 𝑍) |
150 | 149 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → 𝑖 ∈ 𝑍) |
151 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖)) |
152 | 151 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑖 → ((𝐹‘𝑛) ∈ dom 𝑀 ↔ (𝐹‘𝑖) ∈ dom 𝑀)) |
153 | 110, 152 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀))) |
154 | 153, 95 | chvarv 2251 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀) |
155 | 150, 154 | syldan 486 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀) |
156 | 155 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀) |
157 | | fzct 38537 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁...𝑛) ≼ ω |
158 | 157 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ≼ ω) |
159 | 150 | ssd 38278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁...𝑛) ⊆ 𝑍) |
160 | 125 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)) |
161 | 151 | cbvdisjv 4564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Disj 𝑛
∈ 𝑍 (𝐹‘𝑛) ↔ Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖)) |
162 | 160, 161 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖)) |
163 | | disjss1 4559 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁...𝑛) ⊆ 𝑍 → (Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))) |
164 | 159, 162,
163 | sylc 63 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
165 | 164 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
166 | 147, 8, 9, 156, 158, 165 | meadjiun 39359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) =
(Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖))))) |
167 | | fzfid 12634 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ∈ Fin) |
168 | 151 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑖 → (𝑀‘(𝐹‘𝑛)) = (𝑀‘(𝐹‘𝑖))) |
169 | 168 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞) ↔ (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))) |
170 | 110, 169 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)))) |
171 | 170, 102 | chvarv 2251 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)) |
172 | 150, 171 | syldan 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)) |
173 | 172 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)) |
174 | 167, 173 | sge0fsummpt 39283 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) →
(Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖))) |
175 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑚 → (𝐹‘𝑖) = (𝐹‘𝑚)) |
176 | 175 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑚 → (𝑀‘(𝐹‘𝑖)) = (𝑀‘(𝐹‘𝑚))) |
177 | 176 | cbvsumv 14274 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ𝑖 ∈
(𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) |
179 | 174, 178 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) →
(Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) |
180 | 146, 166,
179 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) |
181 | 114, 180 | chvarv 2251 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))) |
182 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
183 | 182 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → (𝑀‘(𝐹‘𝑚)) = (𝑀‘(𝐹‘𝑛))) |
184 | 183 | cbvsumv 14274 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑚 ∈
(𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) |
185 | 184 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))) |
186 | 181, 185 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))) |
187 | 186 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
188 | 187 | ralbidva 2968 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
189 | 188 | biimpd 218 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
190 | 189 | imp 444 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥) |
191 | 108, 190 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥) |
192 | 191 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
193 | 192 | reximdv 2999 |
. . . . . . 7
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
194 | 14, 193 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥) |
195 | 70, 71, 2, 1, 102, 194 | sge0reuzb 39341 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < )) |
196 | 104 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) |
197 | 35, 196 | eqtri 2632 |
. . . . . . . . 9
⊢ 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) |
198 | 197 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))) |
199 | 186 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))) |
200 | 198, 199 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))) |
201 | 200 | rneqd 5274 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 = ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))) |
202 | 201 | supeq1d 8235 |
. . . . 5
⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < )) |
203 | 195, 202 | eqtr4d 2647 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran 𝑆, ℝ, < )) |
204 | 203 | eqcomd 2616 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) =
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛))))) |
205 | 1 | uzct 38257 |
. . . . . 6
⊢ 𝑍 ≼
ω |
206 | 205 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑍 ≼ ω) |
207 | 70, 7, 9, 95, 206, 160 | meadjiun 39359 |
. . . 4
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛)) =
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛))))) |
208 | 207 | eqcomd 2616 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛))) |
209 | 125 | simplrd 789 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
210 | 209 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
211 | 204, 208,
210 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
212 | 69, 211 | breqtrd 4609 |
1
⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |