| Step | Hyp | Ref
| Expression |
| 1 | | meaiuninc3v.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑁 ∈ ℤ) |
| 3 | | meaiuninc3v.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑁) |
| 4 | | meaiuninc3v.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ Meas) |
| 5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas) |
| 6 | | eqid 2737 |
. . . . . 6
⊢ dom 𝑀 = dom 𝑀 |
| 7 | | meaiuninc3v.e |
. . . . . . 7
⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) |
| 8 | 7 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀) |
| 9 | 5, 6, 8 | meaxrcl 46476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈
ℝ*) |
| 10 | | meaiuninc3v.s |
. . . . 5
⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) |
| 11 | 9, 10 | fmptd 7134 |
. . . 4
⊢ (𝜑 → 𝑆:𝑍⟶ℝ*) |
| 12 | 11 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑆:𝑍⟶ℝ*) |
| 13 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑛𝜑 |
| 14 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑛ℝ |
| 15 | | nfra1 3284 |
. . . . . 6
⊢
Ⅎ𝑛∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 |
| 16 | 14, 15 | nfrexw 3313 |
. . . . 5
⊢
Ⅎ𝑛∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 |
| 17 | 13, 16 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑛(𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 18 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑛𝐸 |
| 19 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑀 ∈ Meas) |
| 20 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝐸:𝑍⟶dom 𝑀) |
| 21 | | meaiuninc3v.i |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) |
| 22 | 21 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) |
| 23 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 24 | 17, 18, 19, 2, 3, 20, 22, 23, 10 | meaiunincf 46498 |
. . 3
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑆 ⇝ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 25 | 2, 3, 12, 24 | climxlim2 45861 |
. 2
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑆~~>*(𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 26 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 27 | | 2fveq3 6911 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑛 → (𝑀‘(𝐸‘𝑗)) = (𝑀‘(𝐸‘𝑛))) |
| 28 | 27 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → (𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ 𝑥 < (𝑀‘(𝐸‘𝑛)))) |
| 29 | 28 | cbvrexvw 3238 |
. . . . . . . . . 10
⊢
(∃𝑗 ∈
𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ∃𝑛 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑛))) |
| 30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ∃𝑛 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑛)))) |
| 31 | | rexr 11307 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
| 32 | 31 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ℝ*) |
| 33 | 9 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈
ℝ*) |
| 34 | 32, 33 | xrltnled 45374 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ 𝑍) → (𝑥 < (𝑀‘(𝐸‘𝑛)) ↔ ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
| 35 | 34 | rexbidva 3177 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑛)) ↔ ∃𝑛 ∈ 𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
| 36 | 30, 35 | bitrd 279 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ∃𝑛 ∈ 𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
| 37 | 36 | ralbidva 3176 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ∀𝑥 ∈ ℝ ∃𝑛 ∈ 𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
| 38 | | rexnal 3100 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ¬ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 39 | 38 | ralbii 3093 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ℝ ∃𝑛 ∈
𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑥 ∈ ℝ ¬ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 40 | | ralnex 3072 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ℝ ¬ ∀𝑛
∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 41 | 39, 40 | bitri 275 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℝ ∃𝑛 ∈
𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) |
| 42 | 41 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑛 ∈ 𝑍 ¬ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
| 43 | 37, 42 | bitrd 279 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
| 44 | 43 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)) |
| 45 | 26, 44 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
| 46 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
| 47 | 45, 46 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
| 48 | | simp-4r 784 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑥 ∈ ℝ) |
| 49 | 48, 31 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑥 ∈ ℝ*) |
| 50 | | simp-4l 783 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝜑) |
| 51 | 3 | uztrn2 12897 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ 𝑍) |
| 52 | 51 | ad4ant24 754 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ 𝑍) |
| 53 | 11 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) ∈
ℝ*) |
| 54 | 50, 52, 53 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑆‘𝑛) ∈
ℝ*) |
| 55 | | eleq1w 2824 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍)) |
| 56 | 55 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑗 ∈ 𝑍))) |
| 57 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑗))) |
| 58 | 57 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → ((𝑀‘(𝐸‘𝑛)) ∈ ℝ* ↔ (𝑀‘(𝐸‘𝑗)) ∈
ℝ*)) |
| 59 | 56, 58 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ*) ↔ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑀‘(𝐸‘𝑗)) ∈
ℝ*))) |
| 60 | 59, 9 | chvarvv 1998 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑀‘(𝐸‘𝑗)) ∈
ℝ*) |
| 61 | 60 | ad5ant13 757 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑀‘(𝐸‘𝑗)) ∈
ℝ*) |
| 62 | | simplr 769 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑥 < (𝑀‘(𝐸‘𝑗))) |
| 63 | 4 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑀 ∈ Meas) |
| 64 | 7 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ dom 𝑀) |
| 65 | 64 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐸‘𝑗) ∈ dom 𝑀) |
| 66 | | simp1 1137 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝜑) |
| 67 | 51 | 3adant1 1131 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ 𝑍) |
| 68 | 66, 67, 8 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐸‘𝑛) ∈ dom 𝑀) |
| 69 | | simp3 1139 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ (ℤ≥‘𝑗)) |
| 70 | | simpll 767 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑗..^𝑛)) → 𝜑) |
| 71 | 3 | uzssd3 45437 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ 𝑍 → (ℤ≥‘𝑗) ⊆ 𝑍) |
| 72 | 71 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (𝑗..^𝑛)) → (ℤ≥‘𝑗) ⊆ 𝑍) |
| 73 | | elfzouz 13703 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (𝑗..^𝑛) → 𝑘 ∈ (ℤ≥‘𝑗)) |
| 74 | 73 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (𝑗..^𝑛)) → 𝑘 ∈ (ℤ≥‘𝑗)) |
| 75 | 72, 74 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (𝑗..^𝑛)) → 𝑘 ∈ 𝑍) |
| 76 | 75 | adantll 714 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑗..^𝑛)) → 𝑘 ∈ 𝑍) |
| 77 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → (𝑛 ∈ 𝑍 ↔ 𝑘 ∈ 𝑍)) |
| 78 | 77 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑘 ∈ 𝑍))) |
| 79 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → (𝐸‘𝑛) = (𝐸‘𝑘)) |
| 80 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑘 + 1))) |
| 81 | 79, 80 | sseq12d 4017 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → ((𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)) ↔ (𝐸‘𝑘) ⊆ (𝐸‘(𝑘 + 1)))) |
| 82 | 78, 81 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐸‘𝑘) ⊆ (𝐸‘(𝑘 + 1))))) |
| 83 | 82, 21 | chvarvv 1998 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐸‘𝑘) ⊆ (𝐸‘(𝑘 + 1))) |
| 84 | 70, 76, 83 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑗..^𝑛)) → (𝐸‘𝑘) ⊆ (𝐸‘(𝑘 + 1))) |
| 85 | 84 | 3adantl3 1169 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) ∧ 𝑘 ∈ (𝑗..^𝑛)) → (𝐸‘𝑘) ⊆ (𝐸‘(𝑘 + 1))) |
| 86 | 69, 85 | ssinc 45092 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐸‘𝑗) ⊆ (𝐸‘𝑛)) |
| 87 | 63, 6, 65, 68, 86 | meassle 46478 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑀‘(𝐸‘𝑗)) ≤ (𝑀‘(𝐸‘𝑛))) |
| 88 | | fvexd 6921 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑀‘(𝐸‘𝑛)) ∈ V) |
| 89 | 10 | fvmpt2 7027 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ 𝑍 ∧ (𝑀‘(𝐸‘𝑛)) ∈ V) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛))) |
| 90 | 51, 88, 89 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛))) |
| 91 | 90 | 3adant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛))) |
| 92 | 87, 91 | breqtrrd 5171 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑀‘(𝐸‘𝑗)) ≤ (𝑆‘𝑛)) |
| 93 | 92 | ad5ant135 1370 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑀‘(𝐸‘𝑗)) ≤ (𝑆‘𝑛)) |
| 94 | 49, 61, 54, 62, 93 | xrltletrd 13203 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑥 < (𝑆‘𝑛)) |
| 95 | 49, 54, 94 | xrltled 13192 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑥 ≤ (𝑆‘𝑛)) |
| 96 | 95 | ralrimiva 3146 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛)) |
| 97 | 96 | ex 412 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) → (𝑥 < (𝑀‘(𝐸‘𝑗)) → ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛))) |
| 98 | 97 | reximdva 3168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) → ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛))) |
| 99 | 98 | ralimdva 3167 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛))) |
| 100 | 99 | imp 406 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛)) |
| 101 | | nfmpt1 5250 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) |
| 102 | 10, 101 | nfcxfr 2903 |
. . . . . . 7
⊢
Ⅎ𝑛𝑆 |
| 103 | 102, 1, 3, 11 | xlimpnf 45857 |
. . . . . 6
⊢ (𝜑 → (𝑆~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛))) |
| 104 | 103 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → (𝑆~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝑆‘𝑛))) |
| 105 | 100, 104 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑆~~>*+∞) |
| 106 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥𝜑 |
| 107 | | nfra1 3284 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) |
| 108 | 106, 107 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
| 109 | | rspa 3248 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ ∃𝑗 ∈
𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
| 110 | 109 | adantll 714 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
| 111 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑗𝜑 |
| 112 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗ℝ |
| 113 | | nfre1 3285 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) |
| 114 | 112, 113 | nfralw 3311 |
. . . . . . . . . 10
⊢
Ⅎ𝑗∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) |
| 115 | 111, 114 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑗(𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) |
| 116 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑗 𝑥 ∈ ℝ |
| 117 | 115, 116 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑗((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑥 ∈ ℝ) |
| 118 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑗 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
| 119 | 31 | ad3antlr 731 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑥 ∈ ℝ*) |
| 120 | 4, 6 | dmmeasal 46467 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑀 ∈ SAlg) |
| 121 | 3 | uzct 45068 |
. . . . . . . . . . . . . . 15
⊢ 𝑍 ≼
ω |
| 122 | 121 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ≼ ω) |
| 123 | 120, 122,
8 | saliuncl 46338 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ dom 𝑀) |
| 124 | 4, 6, 123 | meaxrcl 46476 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈
ℝ*) |
| 125 | 124 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈
ℝ*) |
| 126 | 60 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → (𝑀‘(𝐸‘𝑗)) ∈
ℝ*) |
| 127 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑥 < (𝑀‘(𝐸‘𝑗))) |
| 128 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑀 ∈ Meas) |
| 129 | 123 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ dom 𝑀) |
| 130 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝐸‘𝑛) = (𝐸‘𝑗)) |
| 131 | 130 | ssiun2s 5048 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → (𝐸‘𝑗) ⊆ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
| 132 | 131 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ⊆ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
| 133 | 128, 6, 64, 129, 132 | meassle 46478 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑀‘(𝐸‘𝑗)) ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 134 | 133 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → (𝑀‘(𝐸‘𝑗)) ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 135 | 119, 126,
125, 127, 134 | xrltletrd 13203 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑥 < (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 136 | 119, 125,
135 | xrltled 13192 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 137 | 136 | exp31 419 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑗 ∈ 𝑍 → (𝑥 < (𝑀‘(𝐸‘𝑗)) → 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))))) |
| 138 | 137 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑥 ∈ ℝ) → (𝑗 ∈ 𝑍 → (𝑥 < (𝑀‘(𝐸‘𝑗)) → 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))))) |
| 139 | 117, 118,
138 | rexlimd 3266 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗)) → 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) |
| 140 | 110, 139 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) ∧ 𝑥 ∈ ℝ) → 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 141 | 108, 140 | ralrimia 3258 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → ∀𝑥 ∈ ℝ 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 142 | | xrpnf 45496 |
. . . . . . 7
⊢ ((𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈ ℝ* → ((𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) = +∞ ↔ ∀𝑥 ∈ ℝ 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) |
| 143 | 124, 142 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) = +∞ ↔ ∀𝑥 ∈ ℝ 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) |
| 144 | 143 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → ((𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) = +∞ ↔ ∀𝑥 ∈ ℝ 𝑥 ≤ (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) |
| 145 | 141, 144 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) = +∞) |
| 146 | 105, 145 | breqtrrd 5171 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 𝑥 < (𝑀‘(𝐸‘𝑗))) → 𝑆~~>*(𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 147 | 47, 146 | syldan 591 |
. 2
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑆~~>*(𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |
| 148 | 25, 147 | pm2.61dan 813 |
1
⊢ (𝜑 → 𝑆~~>*(𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) |