Step | Hyp | Ref
| Expression |
1 | | meaiuninclem.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑁) |
2 | | meaiuninclem.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
3 | | 0xr 10086 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
4 | 3 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ∈
ℝ*) |
5 | | pnfxr 10092 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
6 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → +∞ ∈
ℝ*) |
7 | | meaiuninclem.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ Meas) |
8 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas) |
9 | | eqid 2622 |
. . . . . . 7
⊢ dom 𝑀 = dom 𝑀 |
10 | | meaiuninclem.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) |
11 | 10 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀) |
12 | 8, 9, 11 | meaxrcl 40678 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈
ℝ*) |
13 | 8, 11 | meage0 40692 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐸‘𝑛))) |
14 | | meaiuninclem.b |
. . . . . . . 8
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
15 | 14 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
16 | | simp1 1061 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝜑 ∧ 𝑛 ∈ 𝑍)) |
17 | | simp2 1062 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ) |
18 | | simp3 1063 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
19 | 16 | simprd 479 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑛 ∈ 𝑍) |
20 | | rspa 2930 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
21 | 18, 19, 20 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
22 | 12 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ∈
ℝ*) |
23 | | rexr 10085 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
24 | 23 | 3ad2ant2 1083 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ*) |
25 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → +∞ ∈
ℝ*) |
26 | | simp3 1063 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
27 | | ltpnf 11954 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 < +∞) |
28 | 27 | 3ad2ant2 1083 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 < +∞) |
29 | 22, 24, 25, 26, 28 | xrlelttrd 11991 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞) |
30 | 16, 17, 21, 29 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞) |
31 | 30 | 3exp 1264 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ ℝ → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞))) |
32 | 31 | rexlimdv 3030 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞)) |
33 | 15, 32 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) < +∞) |
34 | 4, 6, 12, 13, 33 | elicod 12224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ (0[,)+∞)) |
35 | | meaiuninclem.s |
. . . . 5
⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) |
36 | 34, 35 | fmptd 6385 |
. . . 4
⊢ (𝜑 → 𝑆:𝑍⟶(0[,)+∞)) |
37 | | rge0ssre 12280 |
. . . . 5
⊢
(0[,)+∞) ⊆ ℝ |
38 | 37 | a1i 11 |
. . . 4
⊢ (𝜑 → (0[,)+∞) ⊆
ℝ) |
39 | 36, 38 | fssd 6057 |
. . 3
⊢ (𝜑 → 𝑆:𝑍⟶ℝ) |
40 | 1 | peano2uzs 11742 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍) |
41 | 40 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍) |
42 | 10 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀) |
43 | 41, 42 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀) |
44 | | meaiuninclem.i |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) |
45 | 8, 9, 11, 43, 44 | meassle 40680 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1)))) |
46 | 35 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))) |
47 | | fvexd 6203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ V) |
48 | 46, 47 | fvmpt2d 6293 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛))) |
49 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚)) |
50 | 49 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑚))) |
51 | 50 | cbvmptv 4750 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚))) |
52 | 35, 51 | eqtri 2644 |
. . . . . . 7
⊢ 𝑆 = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚))) |
53 | 52 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚)))) |
54 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → (𝐸‘𝑚) = (𝐸‘(𝑛 + 1))) |
55 | 54 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (𝑀‘(𝐸‘𝑚)) = (𝑀‘(𝐸‘(𝑛 + 1)))) |
56 | 55 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 = (𝑛 + 1)) → (𝑀‘(𝐸‘𝑚)) = (𝑀‘(𝐸‘(𝑛 + 1)))) |
57 | | fvexd 6203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘(𝑛 + 1))) ∈ V) |
58 | 53, 56, 41, 57 | fvmptd 6288 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘(𝑛 + 1)) = (𝑀‘(𝐸‘(𝑛 + 1)))) |
59 | 48, 58 | breq12d 4666 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)) ↔ (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1))))) |
60 | 45, 59 | mpbird 247 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1))) |
61 | 48 | eqcomd 2628 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑆‘𝑛)) |
62 | 61 | breq1d 4663 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑆‘𝑛) ≤ 𝑥)) |
63 | 62 | ralbidva 2985 |
. . . . . . 7
⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
64 | 63 | biimpd 219 |
. . . . . 6
⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
65 | 64 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
66 | 65 | reximdva 3017 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)) |
67 | 14, 66 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥) |
68 | 1, 2, 39, 60, 67 | climsup 14400 |
. 2
⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < )) |
69 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑛𝜑 |
70 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
71 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) |
72 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢ (𝐸‘𝑛) ∈ V |
73 | 72 | difexi 4809 |
. . . . . . . . . . . 12
⊢ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V |
74 | 73 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) |
75 | | meaiuninclem.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
76 | 75 | fvmpt2 6291 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
77 | 71, 74, 76 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
78 | 77 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
79 | 7, 9 | dmmeasal 40669 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑀 ∈ SAlg) |
80 | 79 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg) |
81 | | fzoct 39603 |
. . . . . . . . . . . 12
⊢ (𝑁..^𝑛) ≼ ω |
82 | 81 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁..^𝑛) ≼ ω) |
83 | 10 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝐸:𝑍⟶dom 𝑀) |
84 | | fzossuz 39598 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁..^𝑛) ⊆ (ℤ≥‘𝑁) |
85 | 1 | eqcomi 2631 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘𝑁) = 𝑍 |
86 | 84, 85 | sseqtri 3637 |
. . . . . . . . . . . . . . 15
⊢ (𝑁..^𝑛) ⊆ 𝑍 |
87 | 86 | sseli 3599 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ 𝑍) |
88 | 87 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ 𝑍) |
89 | 83, 88 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀) |
90 | 89 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀) |
91 | 80, 82, 90 | saliuncl 40542 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀) |
92 | | saldifcl2 40546 |
. . . . . . . . . 10
⊢ ((dom
𝑀 ∈ SAlg ∧ (𝐸‘𝑛) ∈ dom 𝑀 ∧ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀) |
93 | 80, 11, 91, 92 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀) |
94 | 78, 93 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀) |
95 | 8, 9, 94 | meaxrcl 40678 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈
ℝ*) |
96 | 8, 94 | meage0 40692 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐹‘𝑛))) |
97 | | difssd 3738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛)) |
98 | 78, 97 | eqsstrd 3639 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
99 | 8, 9, 94, 11, 98 | meassle 40680 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ≤ (𝑀‘(𝐸‘𝑛))) |
100 | 95, 12, 6, 99, 33 | xrlelttrd 11991 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) < +∞) |
101 | 4, 6, 95, 96, 100 | elicod 12224 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞)) |
102 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑖 → (𝐸‘𝑛) = (𝐸‘𝑖)) |
103 | 102 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑖 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑖))) |
104 | 103 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)) |
105 | 104 | cbvralv 3171 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) |
106 | 105 | biimpi 206 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) |
107 | 106 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) |
108 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝑛 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍)) |
109 | 108 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑖 ∈ 𝑍))) |
110 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑖 → (𝑁...𝑛) = (𝑁...𝑖)) |
111 | 110 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))) |
112 | 103, 111 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) ↔ (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))) |
113 | 109, 112 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))))) |
114 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑍 ↔ 𝑛 ∈ 𝑍)) |
115 | 114 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑚 ∈ 𝑍) ↔ (𝜑 ∧ 𝑛 ∈ 𝑍))) |
116 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑛 → (𝑁...𝑚) = (𝑁...𝑛)) |
117 | 116 | iuneq1d 4545 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
118 | 116 | iuneq1d 4545 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → ∪
𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)) |
119 | 117, 118 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) ↔ ∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))) |
120 | 115, 119 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) ↔ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)))) |
121 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑛 → (𝐹‘𝑖) = (𝐹‘𝑛)) |
122 | 121 | cbviunv 4559 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) |
123 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) |
124 | 69, 1, 10, 75 | iundjiun 40677 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))) |
125 | 124 | simplld 791 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
126 | 125 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
127 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
128 | | rspa 2930 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑚 ∈
𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ 𝑚 ∈ 𝑍) → ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
129 | 126, 127,
128 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
130 | 102 | cbviunv 4559 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) |
132 | 123, 129,
131 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) |
133 | 120, 132 | chvarv 2263 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)) |
134 | 71, 1 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑁)) |
135 | 134 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ≥‘𝑁)) |
136 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑖 → (𝑛 + 1) = (𝑖 + 1)) |
137 | 136 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑖 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑖 + 1))) |
138 | 102, 137 | sseq12d 3634 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑖 → ((𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)) ↔ (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))) |
139 | 109, 138 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))))) |
140 | 139, 44 | chvarv 2263 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))) |
141 | 88, 140 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))) |
142 | 141 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))) |
143 | 135, 142 | iunincfi 39272 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖) = (𝐸‘𝑛)) |
144 | 133, 143 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
145 | 144 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑀‘∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))) |
146 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖(𝜑 ∧ 𝑛 ∈ 𝑍) |
147 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ (ℤ≥‘𝑁)) |
148 | 147, 85 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ 𝑍) |
149 | 148 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → 𝑖 ∈ 𝑍) |
150 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖)) |
151 | 150 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑖 → ((𝐹‘𝑛) ∈ dom 𝑀 ↔ (𝐹‘𝑖) ∈ dom 𝑀)) |
152 | 109, 151 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀))) |
153 | 152, 94 | chvarv 2263 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀) |
154 | 149, 153 | syldan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀) |
155 | 154 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀) |
156 | | fzct 39596 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁...𝑛) ≼ ω |
157 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ≼ ω) |
158 | 149 | ssd 39252 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁...𝑛) ⊆ 𝑍) |
159 | 124 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)) |
160 | 150 | cbvdisjv 4631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Disj 𝑛
∈ 𝑍 (𝐹‘𝑛) ↔ Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖)) |
161 | 159, 160 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖)) |
162 | | disjss1 4626 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁...𝑛) ⊆ 𝑍 → (Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))) |
163 | 158, 161,
162 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
164 | 163 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) |
165 | 146, 8, 9, 155, 157, 164 | meadjiun 40683 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘∪
𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) =
(Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖))))) |
166 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ∈ Fin) |
167 | 150 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑖 → (𝑀‘(𝐹‘𝑛)) = (𝑀‘(𝐹‘𝑖))) |
168 | 167 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞) ↔ (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))) |
169 | 109, 168 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)))) |
170 | 169, 101 | chvarv 2263 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)) |
171 | 149, 170 | syldan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)) |
172 | 171 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)) |
173 | 166, 172 | sge0fsummpt 40607 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) →
(Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖))) |
174 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑚 → (𝐹‘𝑖) = (𝐹‘𝑚)) |
175 | 174 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑚 → (𝑀‘(𝐹‘𝑖)) = (𝑀‘(𝐹‘𝑚))) |
176 | 175 | cbvsumv 14426 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ𝑖 ∈
(𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) |
178 | 173, 177 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) →
(Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) |
179 | 145, 165,
178 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) |
180 | 113, 179 | chvarv 2263 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))) |
181 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
182 | 181 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → (𝑀‘(𝐹‘𝑚)) = (𝑀‘(𝐹‘𝑛))) |
183 | 182 | cbvsumv 14426 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑚 ∈
(𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) |
184 | 183 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))) |
185 | 180, 184 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))) |
186 | 185 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
187 | 186 | ralbidva 2985 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
188 | 187 | biimpd 219 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
189 | 188 | imp 445 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥) |
190 | 107, 189 | syldan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥) |
191 | 190 | ex 450 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
192 | 191 | reximdv 3016 |
. . . . . . 7
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)) |
193 | 14, 192 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥) |
194 | 69, 70, 2, 1, 101, 193 | sge0reuzb 40665 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < )) |
195 | 103 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) |
196 | 35, 195 | eqtri 2644 |
. . . . . . . . 9
⊢ 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) |
197 | 196 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))) |
198 | 185 | mpteq2dva 4744 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))) |
199 | 197, 198 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))) |
200 | 199 | rneqd 5353 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 = ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))) |
201 | 200 | supeq1d 8352 |
. . . . 5
⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < )) |
202 | 194, 201 | eqtr4d 2659 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran 𝑆, ℝ, < )) |
203 | 202 | eqcomd 2628 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) =
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛))))) |
204 | 1 | uzct 39232 |
. . . . . 6
⊢ 𝑍 ≼
ω |
205 | 204 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑍 ≼ ω) |
206 | 69, 7, 9, 94, 205, 159 | meadjiun 40683 |
. . . 4
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛)) =
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛))))) |
207 | 206 | eqcomd 2628 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛))) |
208 | 124 | simplrd 793 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
209 | 208 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
210 | 203, 207,
209 | 3eqtrd 2660 |
. 2
⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
211 | 68, 210 | breqtrd 4679 |
1
⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |