Step | Hyp | Ref
| Expression |
1 | | carageniuncl.o |
. 2
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
2 | | eqid 2760 |
. 2
⊢ ∪ dom 𝑂 = ∪ dom 𝑂 |
3 | | carageniuncl.s |
. 2
⊢ 𝑆 = (CaraGen‘𝑂) |
4 | | carageniuncl.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸:𝑍⟶𝑆) |
5 | 4 | ffvelrnda 6523 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ 𝑆) |
6 | | elssuni 4619 |
. . . . . . 7
⊢ ((𝐸‘𝑛) ∈ 𝑆 → (𝐸‘𝑛) ⊆ ∪ 𝑆) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ 𝑆) |
8 | 1, 3 | caragenuni 41249 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑆 =
∪ dom 𝑂) |
9 | 8 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑆 = ∪
dom 𝑂) |
10 | 7, 9 | sseqtrd 3782 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
11 | 10 | ralrimiva 3104 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
12 | | iunss 4713 |
. . . 4
⊢ (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂 ↔ ∀𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
13 | 11, 12 | sylibr 224 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
14 | | carageniuncl.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
15 | | fvex 6363 |
. . . . . . 7
⊢
(ℤ≥‘𝑀) ∈ V |
16 | 14, 15 | eqeltri 2835 |
. . . . . 6
⊢ 𝑍 ∈ V |
17 | | fvex 6363 |
. . . . . 6
⊢ (𝐸‘𝑛) ∈ V |
18 | 16, 17 | iunex 7313 |
. . . . 5
⊢ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ V |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ V) |
20 | | elpwg 4310 |
. . . 4
⊢ (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ V → (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝒫 ∪ dom 𝑂 ↔ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂)) |
21 | 19, 20 | syl 17 |
. . 3
⊢ (𝜑 → (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝒫 ∪ dom 𝑂 ↔ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂)) |
22 | 13, 21 | mpbird 247 |
. 2
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝒫 ∪ dom 𝑂) |
23 | | iccssxr 12469 |
. . . . 5
⊢
(0[,]+∞) ⊆ ℝ* |
24 | 1 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑂 ∈ OutMeas) |
25 | | elpwi 4312 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ⊆ ∪ dom
𝑂) |
26 | | ssinss1 3984 |
. . . . . . . 8
⊢ (𝑎 ⊆ ∪ dom 𝑂 → (𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) |
27 | 25, 26 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → (𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) |
28 | 27 | adantl 473 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) |
29 | 24, 2, 28 | omecl 41241 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ (0[,]+∞)) |
30 | 23, 29 | sseldi 3742 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈
ℝ*) |
31 | 25 | adantl 473 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑎 ⊆ ∪ dom
𝑂) |
32 | 31 | ssdifssd 3891 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) |
33 | 24, 2, 32 | omecl 41241 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ (0[,]+∞)) |
34 | 23, 33 | sseldi 3742 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈
ℝ*) |
35 | 30, 34 | xaddcld 12344 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈
ℝ*) |
36 | 24, 2, 31 | omecl 41241 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘𝑎) ∈ (0[,]+∞)) |
37 | 23, 36 | sseldi 3742 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘𝑎) ∈
ℝ*) |
38 | | pnfge 12177 |
. . . . . . 7
⊢ (((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈ ℝ* →
((𝑂‘(𝑎 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ +∞) |
39 | 35, 38 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ +∞) |
40 | 39 | adantr 472 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) = +∞) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ +∞) |
41 | | id 22 |
. . . . . . 7
⊢ ((𝑂‘𝑎) = +∞ → (𝑂‘𝑎) = +∞) |
42 | 41 | eqcomd 2766 |
. . . . . 6
⊢ ((𝑂‘𝑎) = +∞ → +∞ = (𝑂‘𝑎)) |
43 | 42 | adantl 473 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) = +∞) → +∞ = (𝑂‘𝑎)) |
44 | 40, 43 | breqtrd 4830 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) = +∞) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) |
45 | | simpl 474 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂)) |
46 | | rge0ssre 12493 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℝ |
47 | | 0xr 10298 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
48 | 47 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → 0 ∈
ℝ*) |
49 | | pnfxr 10304 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
50 | 49 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → +∞ ∈
ℝ*) |
51 | 45, 36 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ∈ (0[,]+∞)) |
52 | 41 | necon3bi 2958 |
. . . . . . . 8
⊢ (¬
(𝑂‘𝑎) = +∞ → (𝑂‘𝑎) ≠ +∞) |
53 | 52 | adantl 473 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ≠ +∞) |
54 | 48, 50, 51, 53 | eliccelicod 40278 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ∈ (0[,)+∞)) |
55 | 46, 54 | sseldi 3742 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ∈ ℝ) |
56 | 24 | ad2antrr 764 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑂 ∈
OutMeas) |
57 | 31 | ad2antrr 764 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑎 ⊆ ∪ dom 𝑂) |
58 | | simpr 479 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → (𝑂‘𝑎) ∈ ℝ) |
59 | 58 | adantr 472 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → (𝑂‘𝑎) ∈ ℝ) |
60 | | carageniuncl.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
61 | 60 | ad3antrrr 768 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℤ) |
62 | 4 | ad3antrrr 768 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐸:𝑍⟶𝑆) |
63 | | simpr 479 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
64 | | eqid 2760 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) = (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) |
65 | | fveq2 6353 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝐸‘𝑚) = (𝐸‘𝑛)) |
66 | | oveq2 6822 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑀..^𝑚) = (𝑀..^𝑛)) |
67 | 66 | iuneq1d 4697 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ∪
𝑖 ∈ (𝑀..^𝑚)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)) |
68 | 65, 67 | difeq12d 3872 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑀..^𝑚)(𝐸‘𝑖)) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) |
69 | 68 | cbvmptv 4902 |
. . . . . . . 8
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑀..^𝑚)(𝐸‘𝑖))) = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) |
70 | 56, 3, 2, 57, 59, 61, 14, 62, 63, 64, 69 | carageniuncllem2 41260 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥)) |
71 | 70 | ralrimiva 3104 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → ∀𝑥 ∈ ℝ+
((𝑂‘(𝑎 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥)) |
72 | 35 | adantr 472 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈
ℝ*) |
73 | | xralrple 12249 |
. . . . . . 7
⊢ ((((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈ ℝ* ∧ (𝑂‘𝑎) ∈ ℝ) → (((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎) ↔ ∀𝑥 ∈ ℝ+ ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥))) |
74 | 72, 58, 73 | syl2anc 696 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → (((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎) ↔ ∀𝑥 ∈ ℝ+ ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥))) |
75 | 71, 74 | mpbird 247 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) |
76 | 45, 55, 75 | syl2anc 696 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) |
77 | 44, 76 | pm2.61dan 867 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) |
78 | 24, 2, 31 | omelesplit 41256 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘𝑎) ≤ ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))))) |
79 | 35, 37, 77, 78 | xrletrid 12199 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) = (𝑂‘𝑎)) |
80 | 1, 2, 3, 22, 79 | carageneld 41240 |
1
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝑆) |