Step | Hyp | Ref
| Expression |
1 | | meaiuninc3v.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑁 ∈ ℤ) |
3 | | meaiuninc3v.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑁) |
4 | | meaiuninc3v.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ Meas) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas) |
6 | | eqid 2740 |
. . . . . 6
⊢ dom 𝑀 = dom 𝑀 |
7 | | meaiuninc3v.e |
. . . . . . 7
⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) |
8 | 7 | ffvelrnda 6958 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀) |
9 | 5, 6, 8 | meaxrcl 43970 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈
ℝ*) |
10 | | meaiuninc3v.s |
. . . . 5
⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) |
11 | 9, 10 | fmptd 6985 |
. . . 4
⊢ (𝜑 → 𝑆:𝑍⟶ℝ*) |
12 | 11 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑆:𝑍⟶ℝ*) |
13 | | nfv 1921 |
. . . . 5
⊢
Ⅎ𝑛𝜑 |
14 | | nfcv 2909 |
. . . . . 6
⊢
Ⅎ𝑛ℝ |
15 | | nfra1 3145 |
. . . . . 6
⊢
Ⅎ𝑛∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 |
16 | 14, 15 | nfrex 3240 |
. . . . 5
⊢
Ⅎ𝑛∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 |
17 | 13, 16 | nfan 1906 |
. . . 4
⊢
Ⅎ𝑛(𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
18 | | nfcv 2909 |
. . . 4
⊢
Ⅎ𝑛𝐸 |
19 | 4 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑀 ∈ Meas) |
20 | 7 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝐸:𝑍⟶dom 𝑀) |
21 | | meaiuninc3v.i |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) |
22 | 21 | adantlr 712 |
. . . 4
⊢ (((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) |
23 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
24 | 17, 18, 19, 2, 3, 20, 22, 23, 10 | meaiunincf 43992 |
. . 3
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑆 ⇝ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
25 | 2, 3, 12, 24 | climxlim2 43358 |
. 2
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑆~~>*(𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
26 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
27 | | 2fveq3 6776 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑛 → (𝑀‘(𝐸‘𝑗)) = (𝑀‘(𝐸‘𝑛))) |
28 | 27 | breq2d 5091 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → (𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ 𝑥 < (𝑀‘(𝐸‘𝑛)))) |
29 | 28 | cbvrexvw 3382 |
. . . . . . . . . 10
⊢
(∃𝑗 ∈
𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ∃𝑛 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑛))) |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ∃𝑛 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑛)))) |
31 | | rexr 11022 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
32 | 31 | ad2antlr 724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ℝ*) |
33 | 9 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈
ℝ*) |
34 | 32, 33 | xrltnled 42873 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ 𝑍) → (𝑥 < (𝑀‘(𝐸‘𝑛)) ↔ ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
35 | 34 | rexbidva 3227 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑛)) ↔ ∃𝑛 ∈ 𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
36 | 30, 35 | bitrd 278 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ∃𝑛 ∈ 𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
37 | 36 | ralbidva 3122 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ∀𝑥 ∈ ℝ ∃𝑛 ∈ 𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
38 | | rexnal 3168 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ¬ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
39 | 38 | ralbii 3093 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ℝ ∃𝑛 ∈
𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑥 ∈ ℝ ¬ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
40 | | ralnex 3166 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ℝ ¬ ∀𝑛
∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
41 | 39, 40 | bitri 274 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℝ ∃𝑛 ∈
𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
42 | 41 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑛 ∈ 𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
43 | 37, 42 | bitrd 278 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
44 | 43 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
45 | 26, 44 | mpbird 256 |
. . . 4
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
46 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
47 | 45, 46 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
48 | | simp-4r 781 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑥 ∈ ℝ) |
49 | 48, 31 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑥 ∈ ℝ*) |
50 | | simp-4l 780 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝜑) |
51 | 3 | uztrn2 12600 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ 𝑍) |
52 | 51 | ad4ant24 751 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ 𝑍) |
53 | 11 | ffvelrnda 6958 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) ∈
ℝ*) |
54 | 50, 52, 53 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑆‘𝑛) ∈
ℝ*) |
55 | | eleq1w 2823 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍)) |
56 | 55 | anbi2d 629 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑗 ∈ 𝑍))) |
57 | | 2fveq3 6776 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑗))) |
58 | 57 | eleq1d 2825 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → ((𝑀‘(𝐸‘𝑛)) ∈ ℝ* ↔ (𝑀‘(𝐸‘𝑗)) ∈
ℝ*)) |
59 | 56, 58 | imbi12d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ*) ↔ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑀‘(𝐸‘𝑗)) ∈
ℝ*))) |
60 | 59, 9 | chvarvv 2006 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑀‘(𝐸‘𝑗)) ∈
ℝ*) |
61 | 60 | ad5ant13 754 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑀‘(𝐸‘𝑗)) ∈
ℝ*) |
62 | | simplr 766 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑥 < (𝑀‘(𝐸‘𝑗))) |
63 | 4 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑀 ∈ Meas) |
64 | 7 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ dom 𝑀) |
65 | 64 | 3adant3 1131 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐸‘𝑗) ∈ dom 𝑀) |
66 | | simp1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝜑) |
67 | 51 | 3adant1 1129 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ 𝑍) |
68 | 66, 67, 8 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐸‘𝑛) ∈ dom 𝑀) |
69 | | simp3 1137 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ (ℤ≥‘𝑗)) |
70 | | simpll 764 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑗..^𝑛)) → 𝜑) |
71 | 3 | uzssd3 42937 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ 𝑍 → (ℤ≥‘𝑗) ⊆ 𝑍) |
72 | 71 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (𝑗..^𝑛)) → (ℤ≥‘𝑗) ⊆ 𝑍) |
73 | | elfzouz 13390 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (𝑗..^𝑛) → 𝑘 ∈ (ℤ≥‘𝑗)) |
74 | 73 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (𝑗..^𝑛)) → 𝑘 ∈ (ℤ≥‘𝑗)) |
75 | 72, 74 | sseldd 3927 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (𝑗..^𝑛)) → 𝑘 ∈ 𝑍) |
76 | 75 | adantll 711 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑗..^𝑛)) → 𝑘 ∈ 𝑍) |
77 | | eleq1w 2823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → (𝑛 ∈ 𝑍 ↔ 𝑘 ∈ 𝑍)) |
78 | 77 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑘 ∈ 𝑍))) |
79 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → (𝐸‘𝑛) = (𝐸‘𝑘)) |
80 | | fvoveq1 7294 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑘 + 1))) |
81 | 79, 80 | sseq12d 3959 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → ((𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)) ↔ (𝐸‘𝑘) ⊆ (𝐸‘(𝑘 + 1)))) |
82 | 78, 81 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐸‘𝑘) ⊆ (𝐸‘(𝑘 + 1))))) |
83 | 82, 21 | chvarvv 2006 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐸‘𝑘) ⊆ (𝐸‘(𝑘 + 1))) |
84 | 70, 76, 83 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑗..^𝑛)) → (𝐸‘𝑘) ⊆ (𝐸‘(𝑘 + 1))) |
85 | 84 | 3adantl3 1167 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) ∧ 𝑘 ∈ (𝑗..^𝑛)) → (𝐸‘𝑘) ⊆ (𝐸‘(𝑘 + 1))) |
86 | 69, 85 | ssinc 42607 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐸‘𝑗) ⊆ (𝐸‘𝑛)) |
87 | 63, 6, 65, 68, 86 | meassle 43972 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑀‘(𝐸‘𝑗)) ≤ (𝑀‘(𝐸‘𝑛))) |
88 | | fvexd 6786 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑀‘(𝐸‘𝑛)) ∈ V) |
89 | 10 | fvmpt2 6883 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ 𝑍 ∧ (𝑀‘(𝐸‘𝑛)) ∈ V) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛))) |
90 | 51, 88, 89 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛))) |
91 | 90 | 3adant1 1129 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛))) |
92 | 87, 91 | breqtrrd 5107 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑀‘(𝐸‘𝑗)) ≤ (𝑆‘𝑛)) |
93 | 92 | ad5ant135 1367 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑀‘(𝐸‘𝑗)) ≤ (𝑆‘𝑛)) |
94 | 49, 61, 54, 62, 93 | xrltletrd 12894 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑥 < (𝑆‘𝑛)) |
95 | 49, 54, 94 | xrltled 12883 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑥 ≤ (𝑆‘𝑛)) |
96 | 95 | ralrimiva 3110 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛)) |
97 | 96 | ex 413 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) → (𝑥 < (𝑀‘(𝐸‘𝑗)) → ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛))) |
98 | 97 | reximdva 3205 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) → ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛))) |
99 | 98 | ralimdva 3105 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛))) |
100 | 99 | imp 407 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛)) |
101 | | nfmpt1 5187 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) |
102 | 10, 101 | nfcxfr 2907 |
. . . . . . 7
⊢
Ⅎ𝑛𝑆 |
103 | 102, 1, 3, 11 | xlimpnf 43354 |
. . . . . 6
⊢ (𝜑 → (𝑆~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛))) |
104 | 103 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → (𝑆~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛))) |
105 | 100, 104 | mpbird 256 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑆~~>*+∞) |
106 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑥𝜑 |
107 | | nfra1 3145 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) |
108 | 106, 107 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
109 | | rspa 3133 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ ∃𝑗 ∈
𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
110 | 109 | adantll 711 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
111 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑗𝜑 |
112 | | nfcv 2909 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗ℝ |
113 | | nfre1 3237 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) |
114 | 112, 113 | nfralw 3152 |
. . . . . . . . . 10
⊢
Ⅎ𝑗∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) |
115 | 111, 114 | nfan 1906 |
. . . . . . . . 9
⊢
Ⅎ𝑗(𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
116 | | nfv 1921 |
. . . . . . . . 9
⊢
Ⅎ𝑗 𝑥 ∈ ℝ |
117 | 115, 116 | nfan 1906 |
. . . . . . . 8
⊢
Ⅎ𝑗((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑥 ∈ ℝ) |
118 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑗 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
119 | 31 | ad3antlr 728 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑥 ∈ ℝ*) |
120 | 4, 6 | dmmeasal 43961 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑀 ∈ SAlg) |
121 | 3 | uzct 42581 |
. . . . . . . . . . . . . . 15
⊢ 𝑍 ≼
ω |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ≼ ω) |
123 | 120, 122,
8 | saliuncl 43834 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ dom 𝑀) |
124 | 4, 6, 123 | meaxrcl 43970 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈
ℝ*) |
125 | 124 | ad3antrrr 727 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈
ℝ*) |
126 | 60 | ad4ant13 748 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → (𝑀‘(𝐸‘𝑗)) ∈
ℝ*) |
127 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑥 < (𝑀‘(𝐸‘𝑗))) |
128 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑀 ∈ Meas) |
129 | 123 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ dom 𝑀) |
130 | | fveq2 6771 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝐸‘𝑛) = (𝐸‘𝑗)) |
131 | 130 | ssiun2s 4983 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → (𝐸‘𝑗) ⊆ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
132 | 131 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ⊆ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
133 | 128, 6, 64, 129, 132 | meassle 43972 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑀‘(𝐸‘𝑗)) ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
134 | 133 | ad4ant13 748 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → (𝑀‘(𝐸‘𝑗)) ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
135 | 119, 126,
125, 127, 134 | xrltletrd 12894 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑥 < (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
136 | 119, 125,
135 | xrltled 12883 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
137 | 136 | exp31 420 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑗 ∈ 𝑍 → (𝑥 < (𝑀‘(𝐸‘𝑗)) → 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))))) |
138 | 137 | adantlr 712 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑥 ∈ ℝ) → (𝑗 ∈ 𝑍 → (𝑥 < (𝑀‘(𝐸‘𝑗)) → 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))))) |
139 | 117, 118,
138 | rexlimd 3248 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) → 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) |
140 | 110, 139 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑥 ∈ ℝ) → 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
141 | 108, 140 | ralrimia 3429 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → ∀𝑥 ∈ ℝ 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
142 | | xrpnf 42997 |
. . . . . . 7
⊢ ((𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈ ℝ* → ((𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) = +∞ ↔ ∀𝑥 ∈ ℝ 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) |
143 | 124, 142 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) = +∞ ↔ ∀𝑥 ∈ ℝ 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) |
144 | 143 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → ((𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) = +∞ ↔ ∀𝑥 ∈ ℝ 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) |
145 | 141, 144 | mpbird 256 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) = +∞) |
146 | 105, 145 | breqtrrd 5107 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑆~~>*(𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
147 | 47, 146 | syldan 591 |
. 2
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑆~~>*(𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
148 | 25, 147 | pm2.61dan 810 |
1
⊢ (𝜑 → 𝑆~~>*(𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |