| Step | Hyp | Ref
| Expression |
| 1 | | inss1 4237 |
. . . 4
⊢ (𝐸 ∩ 𝐴) ⊆ 𝐸 |
| 2 | | uniioombl.s |
. . . . 5
⊢ (𝜑 → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
| 3 | | uniioombl.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 4 | 3 | uniiccdif 25613 |
. . . . . . 7
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺) ∧
(vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran
((,) ∘ 𝐺))) =
0)) |
| 5 | 4 | simpld 494 |
. . . . . 6
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺)) |
| 6 | | ovolficcss 25504 |
. . . . . . 7
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐺) ⊆
ℝ) |
| 7 | 3, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ) |
| 8 | 5, 7 | sstrd 3994 |
. . . . 5
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ) |
| 9 | 2, 8 | sstrd 3994 |
. . . 4
⊢ (𝜑 → 𝐸 ⊆ ℝ) |
| 10 | | uniioombl.e |
. . . 4
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) |
| 11 | | ovolsscl 25521 |
. . . 4
⊢ (((𝐸 ∩ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∩ 𝐴)) ∈
ℝ) |
| 12 | 1, 9, 10, 11 | mp3an2i 1468 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ) |
| 13 | | difssd 4137 |
. . . 4
⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ 𝐸) |
| 14 | | ovolsscl 25521 |
. . . 4
⊢ (((𝐸 ∖ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) →
(vol*‘(𝐸 ∖
𝐴)) ∈
ℝ) |
| 15 | 13, 9, 10, 14 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ) |
| 16 | 12, 15 | readdcld 11290 |
. 2
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ∈ ℝ) |
| 17 | | inss1 4237 |
. . . . 5
⊢ (𝐾 ∩ 𝐴) ⊆ 𝐾 |
| 18 | | uniioombl.k |
. . . . . . 7
⊢ 𝐾 = ∪
(((,) ∘ 𝐺) “
(1...𝑀)) |
| 19 | | imassrn 6089 |
. . . . . . . 8
⊢ (((,)
∘ 𝐺) “
(1...𝑀)) ⊆ ran ((,)
∘ 𝐺) |
| 20 | 19 | unissi 4916 |
. . . . . . 7
⊢ ∪ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ∪ ran
((,) ∘ 𝐺) |
| 21 | 18, 20 | eqsstri 4030 |
. . . . . 6
⊢ 𝐾 ⊆ ∪ ran ((,) ∘ 𝐺) |
| 22 | 21, 8 | sstrid 3995 |
. . . . 5
⊢ (𝜑 → 𝐾 ⊆ ℝ) |
| 23 | | uniioombl.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 24 | | uniioombl.2 |
. . . . . . . 8
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
| 25 | | uniioombl.3 |
. . . . . . . 8
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
| 26 | | uniioombl.a |
. . . . . . . 8
⊢ 𝐴 = ∪
ran ((,) ∘ 𝐹) |
| 27 | | uniioombl.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
| 28 | | uniioombl.t |
. . . . . . . 8
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
| 29 | | uniioombl.v |
. . . . . . . 8
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐸) + 𝐶)) |
| 30 | 23, 24, 25, 26, 10, 27, 3, 2, 28, 29 | uniioombllem1 25616 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
| 31 | | ssid 4006 |
. . . . . . . 8
⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
((,) ∘ 𝐺) |
| 32 | 28 | ovollb 25514 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ((,) ∘
𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
| 33 | 3, 31, 32 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
| 34 | | ovollecl 25518 |
. . . . . . 7
⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < )
∈ ℝ ∧ (vol*‘∪ ran ((,) ∘
𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
→ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈
ℝ) |
| 35 | 8, 30, 33, 34 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) |
| 36 | | ovolsscl 25521 |
. . . . . 6
⊢ ((𝐾 ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘𝐾) ∈
ℝ) |
| 37 | 21, 8, 35, 36 | mp3an2i 1468 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐾) ∈
ℝ) |
| 38 | | ovolsscl 25521 |
. . . . 5
⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∩ 𝐴)) ∈
ℝ) |
| 39 | 17, 22, 37, 38 | mp3an2i 1468 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) |
| 40 | | difssd 4137 |
. . . . 5
⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ 𝐾) |
| 41 | | ovolsscl 25521 |
. . . . 5
⊢ (((𝐾 ∖ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∖
𝐴)) ∈
ℝ) |
| 42 | 40, 22, 37, 41 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ) |
| 43 | 39, 42 | readdcld 11290 |
. . 3
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) ∈ ℝ) |
| 44 | 27 | rpred 13077 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 45 | 44, 44 | readdcld 11290 |
. . 3
⊢ (𝜑 → (𝐶 + 𝐶) ∈ ℝ) |
| 46 | 43, 45 | readdcld 11290 |
. 2
⊢ (𝜑 → (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)) ∈ ℝ) |
| 47 | | 4re 12350 |
. . . 4
⊢ 4 ∈
ℝ |
| 48 | | remulcl 11240 |
. . . 4
⊢ ((4
∈ ℝ ∧ 𝐶
∈ ℝ) → (4 · 𝐶) ∈ ℝ) |
| 49 | 47, 44, 48 | sylancr 587 |
. . 3
⊢ (𝜑 → (4 · 𝐶) ∈
ℝ) |
| 50 | 10, 49 | readdcld 11290 |
. 2
⊢ (𝜑 → ((vol*‘𝐸) + (4 · 𝐶)) ∈
ℝ) |
| 51 | | uniioombl.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 52 | | uniioombl.m2 |
. . . 4
⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) |
| 53 | 23, 24, 25, 26, 10, 27, 3, 2, 28, 29, 51, 52, 18 | uniioombllem3 25620 |
. . 3
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶))) |
| 54 | 16, 46, 53 | ltled 11409 |
. 2
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶))) |
| 55 | 10, 45 | readdcld 11290 |
. . . 4
⊢ (𝜑 → ((vol*‘𝐸) + (𝐶 + 𝐶)) ∈ ℝ) |
| 56 | 37, 44 | readdcld 11290 |
. . . . 5
⊢ (𝜑 → ((vol*‘𝐾) + 𝐶) ∈ ℝ) |
| 57 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝐾 ∩ 𝐿) ⊆ 𝐾 |
| 58 | | ovolsscl 25521 |
. . . . . . . . 9
⊢ (((𝐾 ∩ 𝐿) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∩ 𝐿)) ∈
ℝ) |
| 59 | 57, 22, 37, 58 | mp3an2i 1468 |
. . . . . . . 8
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐿)) ∈ ℝ) |
| 60 | 59, 44 | readdcld 11290 |
. . . . . . 7
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶) ∈ ℝ) |
| 61 | | difssd 4137 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∖ 𝐿) ⊆ 𝐾) |
| 62 | | ovolsscl 25521 |
. . . . . . . 8
⊢ (((𝐾 ∖ 𝐿) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∖
𝐿)) ∈
ℝ) |
| 63 | 61, 22, 37, 62 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐿)) ∈ ℝ) |
| 64 | | uniioombl.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 65 | | uniioombl.n2 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀)) |
| 66 | | uniioombl.l |
. . . . . . . 8
⊢ 𝐿 = ∪
(((,) ∘ 𝐹) “
(1...𝑁)) |
| 67 | 23, 24, 25, 26, 10, 27, 3, 2, 28, 29, 51, 52, 18, 64, 65, 66 | uniioombllem4 25621 |
. . . . . . 7
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶)) |
| 68 | | imassrn 6089 |
. . . . . . . . . . 11
⊢ (((,)
∘ 𝐹) “
(1...𝑁)) ⊆ ran ((,)
∘ 𝐹) |
| 69 | 68 | unissi 4916 |
. . . . . . . . . 10
⊢ ∪ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ∪ ran
((,) ∘ 𝐹) |
| 70 | 69, 66, 26 | 3sstr4i 4035 |
. . . . . . . . 9
⊢ 𝐿 ⊆ 𝐴 |
| 71 | | sscon 4143 |
. . . . . . . . 9
⊢ (𝐿 ⊆ 𝐴 → (𝐾 ∖ 𝐴) ⊆ (𝐾 ∖ 𝐿)) |
| 72 | 70, 71 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ (𝐾 ∖ 𝐿)) |
| 73 | 61, 22 | sstrd 3994 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∖ 𝐿) ⊆ ℝ) |
| 74 | | ovolss 25520 |
. . . . . . . 8
⊢ (((𝐾 ∖ 𝐴) ⊆ (𝐾 ∖ 𝐿) ∧ (𝐾 ∖ 𝐿) ⊆ ℝ) → (vol*‘(𝐾 ∖ 𝐴)) ≤ (vol*‘(𝐾 ∖ 𝐿))) |
| 75 | 72, 73, 74 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ≤ (vol*‘(𝐾 ∖ 𝐿))) |
| 76 | 39, 42, 60, 63, 67, 75 | le2addd 11882 |
. . . . . 6
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) ≤ (((vol*‘(𝐾 ∩ 𝐿)) + 𝐶) + (vol*‘(𝐾 ∖ 𝐿)))) |
| 77 | 59 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐿)) ∈ ℂ) |
| 78 | 44 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 79 | 63 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐿)) ∈ ℂ) |
| 80 | 77, 78, 79 | add32d 11489 |
. . . . . . 7
⊢ (𝜑 → (((vol*‘(𝐾 ∩ 𝐿)) + 𝐶) + (vol*‘(𝐾 ∖ 𝐿))) = (((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘(𝐾 ∖ 𝐿))) + 𝐶)) |
| 81 | | ioof 13487 |
. . . . . . . . . . . . 13
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 82 | | inss2 4238 |
. . . . . . . . . . . . . . 15
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 83 | | rexpssxrxp 11306 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 84 | 82, 83 | sstri 3993 |
. . . . . . . . . . . . . 14
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 85 | | fss 6752 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 86 | 23, 84, 85 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 87 | | fco 6760 |
. . . . . . . . . . . . 13
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
| 88 | 81, 86, 87 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
| 89 | | ffun 6739 |
. . . . . . . . . . . 12
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
Fun ((,) ∘ 𝐹)) |
| 90 | | funiunfv 7268 |
. . . . . . . . . . . 12
⊢ (Fun ((,)
∘ 𝐹) → ∪ 𝑛 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑛) = ∪ (((,)
∘ 𝐹) “
(1...𝑁))) |
| 91 | 88, 89, 90 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑛) = ∪ (((,)
∘ 𝐹) “
(1...𝑁))) |
| 92 | 91, 66 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑛) = 𝐿) |
| 93 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
| 94 | | elfznn 13593 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ) |
| 95 | | fvco3 7008 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
| 96 | 23, 94, 95 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
| 97 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 98 | 23, 94, 97 | syl2an 596 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐹‘𝑛) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 99 | 98 | elin2d 4205 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐹‘𝑛) ∈ (ℝ ×
ℝ)) |
| 100 | | 1st2nd2 8053 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑛) ∈ (ℝ × ℝ) →
(𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
| 101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
| 102 | 101 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
| 103 | | df-ov 7434 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
| 104 | 102, 103 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑛)) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))) |
| 105 | 96, 104 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))) |
| 106 | | ioombl 25600 |
. . . . . . . . . . . . 13
⊢
((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol |
| 107 | 105, 106 | eqeltrdi 2849 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
| 108 | 107 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
| 109 | | finiunmbl 25579 |
. . . . . . . . . . 11
⊢
(((1...𝑁) ∈ Fin
∧ ∀𝑛 ∈
(1...𝑁)(((,) ∘ 𝐹)‘𝑛) ∈ dom vol) → ∪ 𝑛 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
| 110 | 93, 108, 109 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
| 111 | 92, 110 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ dom vol) |
| 112 | | mblsplit 25567 |
. . . . . . . . 9
⊢ ((𝐿 ∈ dom vol ∧ 𝐾 ⊆ ℝ ∧
(vol*‘𝐾) ∈
ℝ) → (vol*‘𝐾) = ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘(𝐾 ∖ 𝐿)))) |
| 113 | 111, 22, 37, 112 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (vol*‘𝐾) = ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘(𝐾 ∖ 𝐿)))) |
| 114 | 113 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((vol*‘𝐾) + 𝐶) = (((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘(𝐾 ∖ 𝐿))) + 𝐶)) |
| 115 | 80, 114 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → (((vol*‘(𝐾 ∩ 𝐿)) + 𝐶) + (vol*‘(𝐾 ∖ 𝐿))) = ((vol*‘𝐾) + 𝐶)) |
| 116 | 76, 115 | breqtrd 5169 |
. . . . 5
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) ≤ ((vol*‘𝐾) + 𝐶)) |
| 117 | 10, 44 | readdcld 11290 |
. . . . . . 7
⊢ (𝜑 → ((vol*‘𝐸) + 𝐶) ∈ ℝ) |
| 118 | 28 | ovollb 25514 |
. . . . . . . . 9
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐾 ⊆ ∪ ran
((,) ∘ 𝐺)) →
(vol*‘𝐾) ≤ sup(ran
𝑇, ℝ*,
< )) |
| 119 | 3, 21, 118 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (vol*‘𝐾) ≤ sup(ran 𝑇, ℝ*, <
)) |
| 120 | 37, 30, 117, 119, 29 | letrd 11418 |
. . . . . . 7
⊢ (𝜑 → (vol*‘𝐾) ≤ ((vol*‘𝐸) + 𝐶)) |
| 121 | 37, 117, 44, 120 | leadd1dd 11877 |
. . . . . 6
⊢ (𝜑 → ((vol*‘𝐾) + 𝐶) ≤ (((vol*‘𝐸) + 𝐶) + 𝐶)) |
| 122 | 10 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → (vol*‘𝐸) ∈
ℂ) |
| 123 | 122, 78, 78 | addassd 11283 |
. . . . . 6
⊢ (𝜑 → (((vol*‘𝐸) + 𝐶) + 𝐶) = ((vol*‘𝐸) + (𝐶 + 𝐶))) |
| 124 | 121, 123 | breqtrd 5169 |
. . . . 5
⊢ (𝜑 → ((vol*‘𝐾) + 𝐶) ≤ ((vol*‘𝐸) + (𝐶 + 𝐶))) |
| 125 | 43, 56, 55, 116, 124 | letrd 11418 |
. . . 4
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (𝐶 + 𝐶))) |
| 126 | 43, 55, 45, 125 | leadd1dd 11877 |
. . 3
⊢ (𝜑 → (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)) ≤ (((vol*‘𝐸) + (𝐶 + 𝐶)) + (𝐶 + 𝐶))) |
| 127 | 45 | recnd 11289 |
. . . . 5
⊢ (𝜑 → (𝐶 + 𝐶) ∈ ℂ) |
| 128 | 122, 127,
127 | addassd 11283 |
. . . 4
⊢ (𝜑 → (((vol*‘𝐸) + (𝐶 + 𝐶)) + (𝐶 + 𝐶)) = ((vol*‘𝐸) + ((𝐶 + 𝐶) + (𝐶 + 𝐶)))) |
| 129 | | 2t2e4 12430 |
. . . . . . 7
⊢ (2
· 2) = 4 |
| 130 | 129 | oveq1i 7441 |
. . . . . 6
⊢ ((2
· 2) · 𝐶) =
(4 · 𝐶) |
| 131 | | 2cnd 12344 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℂ) |
| 132 | 131, 131,
78 | mulassd 11284 |
. . . . . . 7
⊢ (𝜑 → ((2 · 2) ·
𝐶) = (2 · (2
· 𝐶))) |
| 133 | 78 | 2timesd 12509 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝐶) = (𝐶 + 𝐶)) |
| 134 | 133 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (2 · (2 ·
𝐶)) = (2 · (𝐶 + 𝐶))) |
| 135 | 127 | 2timesd 12509 |
. . . . . . 7
⊢ (𝜑 → (2 · (𝐶 + 𝐶)) = ((𝐶 + 𝐶) + (𝐶 + 𝐶))) |
| 136 | 132, 134,
135 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → ((2 · 2) ·
𝐶) = ((𝐶 + 𝐶) + (𝐶 + 𝐶))) |
| 137 | 130, 136 | eqtr3id 2791 |
. . . . 5
⊢ (𝜑 → (4 · 𝐶) = ((𝐶 + 𝐶) + (𝐶 + 𝐶))) |
| 138 | 137 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → ((vol*‘𝐸) + (4 · 𝐶)) = ((vol*‘𝐸) + ((𝐶 + 𝐶) + (𝐶 + 𝐶)))) |
| 139 | 128, 138 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → (((vol*‘𝐸) + (𝐶 + 𝐶)) + (𝐶 + 𝐶)) = ((vol*‘𝐸) + (4 · 𝐶))) |
| 140 | 126, 139 | breqtrd 5169 |
. 2
⊢ (𝜑 → (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)) ≤ ((vol*‘𝐸) + (4 · 𝐶))) |
| 141 | 16, 46, 50, 54, 140 | letrd 11418 |
1
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) |