Proof of Theorem uniioombllem4
| Step | Hyp | Ref
| Expression |
| 1 | | inss1 4237 |
. . 3
⊢ (𝐾 ∩ 𝐴) ⊆ 𝐾 |
| 2 | | uniioombl.k |
. . . . 5
⊢ 𝐾 = ∪
(((,) ∘ 𝐺) “
(1...𝑀)) |
| 3 | | imassrn 6089 |
. . . . . 6
⊢ (((,)
∘ 𝐺) “
(1...𝑀)) ⊆ ran ((,)
∘ 𝐺) |
| 4 | 3 | unissi 4916 |
. . . . 5
⊢ ∪ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ∪ ran
((,) ∘ 𝐺) |
| 5 | 2, 4 | eqsstri 4030 |
. . . 4
⊢ 𝐾 ⊆ ∪ ran ((,) ∘ 𝐺) |
| 6 | | uniioombl.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 7 | 6 | uniiccdif 25613 |
. . . . . 6
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺) ∧
(vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran
((,) ∘ 𝐺))) =
0)) |
| 8 | 7 | simpld 494 |
. . . . 5
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺)) |
| 9 | | ovolficcss 25504 |
. . . . . 6
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐺) ⊆
ℝ) |
| 10 | 6, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ) |
| 11 | 8, 10 | sstrd 3994 |
. . . 4
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ) |
| 12 | 5, 11 | sstrid 3995 |
. . 3
⊢ (𝜑 → 𝐾 ⊆ ℝ) |
| 13 | | uniioombl.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 14 | | uniioombl.2 |
. . . . . 6
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
| 15 | | uniioombl.3 |
. . . . . 6
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
| 16 | | uniioombl.a |
. . . . . 6
⊢ 𝐴 = ∪
ran ((,) ∘ 𝐹) |
| 17 | | uniioombl.e |
. . . . . 6
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) |
| 18 | | uniioombl.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
| 19 | | uniioombl.s |
. . . . . 6
⊢ (𝜑 → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
| 20 | | uniioombl.t |
. . . . . 6
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
| 21 | | uniioombl.v |
. . . . . 6
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐸) + 𝐶)) |
| 22 | 13, 14, 15, 16, 17, 18, 6, 19, 20, 21 | uniioombllem1 25616 |
. . . . 5
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
| 23 | | ssid 4006 |
. . . . . 6
⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
((,) ∘ 𝐺) |
| 24 | 20 | ovollb 25514 |
. . . . . 6
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ((,) ∘
𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
| 25 | 6, 23, 24 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
| 26 | | ovollecl 25518 |
. . . . 5
⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < )
∈ ℝ ∧ (vol*‘∪ ran ((,) ∘
𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
→ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈
ℝ) |
| 27 | 11, 22, 25, 26 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) |
| 28 | | ovolsscl 25521 |
. . . 4
⊢ ((𝐾 ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘𝐾) ∈
ℝ) |
| 29 | 5, 11, 27, 28 | mp3an2i 1468 |
. . 3
⊢ (𝜑 → (vol*‘𝐾) ∈
ℝ) |
| 30 | | ovolsscl 25521 |
. . 3
⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∩ 𝐴)) ∈
ℝ) |
| 31 | 1, 12, 29, 30 | mp3an2i 1468 |
. 2
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) |
| 32 | | inss1 4237 |
. . . 4
⊢ (𝐾 ∩ 𝐿) ⊆ 𝐾 |
| 33 | | ovolsscl 25521 |
. . . 4
⊢ (((𝐾 ∩ 𝐿) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∩ 𝐿)) ∈
ℝ) |
| 34 | 32, 12, 29, 33 | mp3an2i 1468 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐿)) ∈ ℝ) |
| 35 | | ssun2 4179 |
. . . . . 6
⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((𝐾 ∩ 𝐿) ∪ ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 36 | | nnuz 12921 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
| 37 | | uniioombl.n |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 38 | 37 | peano2nnd 12283 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 + 1) ∈ ℕ) |
| 39 | 38, 36 | eleqtrdi 2851 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘1)) |
| 40 | | uzsplit 13636 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 + 1) ∈
(ℤ≥‘1) → (ℤ≥‘1) =
((1...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
| 41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(ℤ≥‘1) = ((1...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1)))) |
| 42 | 36, 41 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ = ((1...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1)))) |
| 43 | 37 | nncnd 12282 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 44 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
| 45 | | pncan 11514 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
| 46 | 43, 44, 45 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
| 47 | 46 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...((𝑁 + 1) − 1)) = (1...𝑁)) |
| 48 | 47 | uneq1d 4167 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1))) = ((1...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) |
| 49 | 42, 48 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℕ = ((1...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))) |
| 50 | 49 | iuneq1d 5019 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = ∪
𝑖 ∈ ((1...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖))) |
| 51 | | iunxun 5094 |
. . . . . . . . . . 11
⊢ ∪ 𝑖 ∈ ((1...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖)) = (∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
| 52 | 50, 51 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = (∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
| 53 | | ioof 13487 |
. . . . . . . . . . . . . 14
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 54 | | inss2 4238 |
. . . . . . . . . . . . . . . 16
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 55 | | rexpssxrxp 11306 |
. . . . . . . . . . . . . . . 16
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 56 | 54, 55 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 57 | | fss 6752 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 58 | 13, 56, 57 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 59 | | fco 6760 |
. . . . . . . . . . . . . 14
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
| 60 | 53, 58, 59 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
| 61 | | ffn 6736 |
. . . . . . . . . . . . 13
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
((,) ∘ 𝐹) Fn
ℕ) |
| 62 | | fniunfv 7267 |
. . . . . . . . . . . . 13
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,)
∘ 𝐹)) |
| 63 | 60, 61, 62 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,)
∘ 𝐹)) |
| 64 | | fvco3 7008 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖))) |
| 65 | 13, 64 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖))) |
| 66 | 65 | iuneq2dv 5016 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ ℕ
((,)‘(𝐹‘𝑖))) |
| 67 | 63, 66 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪
𝑖 ∈ ℕ
((,)‘(𝐹‘𝑖))) |
| 68 | 16, 67 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = ∪ 𝑖 ∈ ℕ
((,)‘(𝐹‘𝑖))) |
| 69 | | uniioombl.l |
. . . . . . . . . . . 12
⊢ 𝐿 = ∪
(((,) ∘ 𝐹) “
(1...𝑁)) |
| 70 | | ffun 6739 |
. . . . . . . . . . . . . 14
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
Fun ((,) ∘ 𝐹)) |
| 71 | | funiunfv 7268 |
. . . . . . . . . . . . . 14
⊢ (Fun ((,)
∘ 𝐹) → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,)
∘ 𝐹) “
(1...𝑁))) |
| 72 | 60, 70, 71 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,)
∘ 𝐹) “
(1...𝑁))) |
| 73 | | elfznn 13593 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ) |
| 74 | 13, 73, 64 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖))) |
| 75 | 74 | iuneq2dv 5016 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))) |
| 76 | 72, 75 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ (((,) ∘ 𝐹) “ (1...𝑁)) = ∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))) |
| 77 | 69, 76 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))) |
| 78 | 77 | uneq1d 4167 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
| 79 | 52, 68, 78 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
| 80 | 79 | ineq2d 4220 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∩ 𝐴) = (𝐾 ∩ (𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))) |
| 81 | | indi 4284 |
. . . . . . . 8
⊢ (𝐾 ∩ (𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
| 82 | 80, 81 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))) |
| 83 | | fss 6752 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
| 84 | 6, 56, 83 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
| 85 | | fco 6760 |
. . . . . . . . . . . . . 14
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐺:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
| 86 | 53, 84, 85 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
| 87 | | ffun 6739 |
. . . . . . . . . . . . 13
⊢ (((,)
∘ 𝐺):ℕ⟶𝒫 ℝ →
Fun ((,) ∘ 𝐺)) |
| 88 | | funiunfv 7268 |
. . . . . . . . . . . . 13
⊢ (Fun ((,)
∘ 𝐺) → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,)
∘ 𝐺) “
(1...𝑀))) |
| 89 | 86, 87, 88 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,)
∘ 𝐺) “
(1...𝑀))) |
| 90 | | elfznn 13593 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
| 91 | | fvco3 7008 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗))) |
| 92 | 6, 90, 91 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗))) |
| 93 | 92 | iuneq2dv 5016 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
| 94 | 89, 93 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (1...𝑀)) = ∪
𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
| 95 | 2, 94 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
| 96 | 95 | ineq2d 4220 |
. . . . . . . . 9
⊢ (𝜑 → (∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾) = (∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪
𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))) |
| 97 | | incom 4209 |
. . . . . . . . 9
⊢ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾) |
| 98 | | iunin2 5071 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
| 99 | | incom 4209 |
. . . . . . . . . . . . . . 15
⊢
(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) |
| 100 | 99 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈
(ℤ≥‘(𝑁 + 1)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))) |
| 101 | 100 | iuneq2i 5013 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) |
| 102 | | incom 4209 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
| 103 | 98, 101, 102 | 3eqtr4ri 2776 |
. . . . . . . . . . . 12
⊢ (∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) |
| 104 | 103 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → (∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 105 | 104 | iuneq2i 5013 |
. . . . . . . . . 10
⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) |
| 106 | | iunin2 5071 |
. . . . . . . . . 10
⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪
𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
| 107 | 105, 106 | eqtr3i 2767 |
. . . . . . . . 9
⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪
𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
| 108 | 96, 97, 107 | 3eqtr4g 2802 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 109 | 108 | uneq2d 4168 |
. . . . . . 7
⊢ (𝜑 → ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 110 | 82, 109 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 111 | 35, 110 | sseqtrrid 4027 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ (𝐾 ∩ 𝐴)) |
| 112 | 111, 1 | sstrdi 3996 |
. . . 4
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾) |
| 113 | | ovolsscl 25521 |
. . . 4
⊢
((∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 114 | 112, 12, 29, 113 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 115 | 34, 114 | readdcld 11290 |
. 2
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ∈ ℝ) |
| 116 | 18 | rpred 13077 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 117 | 34, 116 | readdcld 11290 |
. 2
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶) ∈ ℝ) |
| 118 | 110 | fveq2d 6910 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) = (vol*‘((𝐾 ∩ 𝐿) ∪ ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
| 119 | 32, 12 | sstrid 3995 |
. . . 4
⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ ℝ) |
| 120 | 112, 12 | sstrd 3994 |
. . . 4
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ) |
| 121 | | ovolun 25534 |
. . . 4
⊢ ((((𝐾 ∩ 𝐿) ⊆ ℝ ∧ (vol*‘(𝐾 ∩ 𝐿)) ∈ ℝ) ∧ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧
(vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) →
(vol*‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
| 122 | 119, 34, 120, 114, 121 | syl22anc 839 |
. . 3
⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐿) ∪ ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
| 123 | 118, 122 | eqbrtrd 5165 |
. 2
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
| 124 | | fzfid 14014 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
| 125 | | iunss 5045 |
. . . . . . . 8
⊢ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ↔ ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾) |
| 126 | 112, 125 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾) |
| 127 | 126 | r19.21bi 3251 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾) |
| 128 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐾 ⊆ ℝ) |
| 129 | 29 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘𝐾) ∈ ℝ) |
| 130 | | ovolsscl 25521 |
. . . . . 6
⊢
((∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 131 | 127, 128,
129, 130 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 132 | 124, 131 | fsumrecl 15770 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 133 | 127, 128 | sstrd 3994 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ) |
| 134 | 133, 131 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧
(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) |
| 135 | 134 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧
(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) |
| 136 | | ovolfiniun 25536 |
. . . . 5
⊢
(((1...𝑀) ∈ Fin
∧ ∀𝑗 ∈
(1...𝑀)(∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧
(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) →
(vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 137 | 124, 135,
136 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 138 | | uniioombl.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 139 | 116, 138 | nndivred 12320 |
. . . . . . 7
⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℝ) |
| 140 | 139 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶 / 𝑀) ∈ ℝ) |
| 141 | 77 | ineq2d 4220 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))) |
| 142 | 141 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))) |
| 143 | 99 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...𝑁) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))) |
| 144 | 143 | iuneq2i 5013 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) |
| 145 | | iunin2 5071 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))) |
| 146 | 144, 145 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))) |
| 147 | 142, 146 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = ∪
𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 148 | | fzfid 14014 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1...𝑁) ∈ Fin) |
| 149 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 150 | 13, 73, 149 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 151 | 150 | elin2d 4205 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ (ℝ ×
ℝ)) |
| 152 | | 1st2nd2 8053 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑖) ∈ (ℝ × ℝ) →
(𝐹‘𝑖) = 〈(1st ‘(𝐹‘𝑖)), (2nd ‘(𝐹‘𝑖))〉) |
| 153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) = 〈(1st ‘(𝐹‘𝑖)), (2nd ‘(𝐹‘𝑖))〉) |
| 154 | 153 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((,)‘〈(1st
‘(𝐹‘𝑖)), (2nd
‘(𝐹‘𝑖))〉)) |
| 155 | | df-ov 7434 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(𝐹‘𝑖))(,)(2nd ‘(𝐹‘𝑖))) = ((,)‘〈(1st
‘(𝐹‘𝑖)), (2nd
‘(𝐹‘𝑖))〉) |
| 156 | 154, 155 | eqtr4di 2795 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((1st ‘(𝐹‘𝑖))(,)(2nd ‘(𝐹‘𝑖)))) |
| 157 | | ioombl 25600 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝐹‘𝑖))(,)(2nd ‘(𝐹‘𝑖))) ∈ dom vol |
| 158 | 156, 157 | eqeltrdi 2849 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol) |
| 159 | 158 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol) |
| 160 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 161 | 6, 90, 160 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 162 | 161 | elin2d 4205 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ ×
ℝ)) |
| 163 | | 1st2nd2 8053 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) →
(𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
| 164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
| 165 | 164 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉)) |
| 166 | | df-ov 7434 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉) |
| 167 | 165, 166 | eqtr4di 2795 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗)))) |
| 168 | | ioombl 25600 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ∈ dom vol |
| 169 | 167, 168 | eqeltrdi 2849 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol) |
| 170 | 169 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol) |
| 171 | | inmbl 25577 |
. . . . . . . . . . . . . 14
⊢
((((,)‘(𝐹‘𝑖)) ∈ dom vol ∧ ((,)‘(𝐺‘𝑗)) ∈ dom vol) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) |
| 172 | 159, 170,
171 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) |
| 173 | 172 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) |
| 174 | | finiunmbl 25579 |
. . . . . . . . . . . 12
⊢
(((1...𝑁) ∈ Fin
∧ ∀𝑖 ∈
(1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) |
| 175 | 148, 173,
174 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) |
| 176 | 147, 175 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol) |
| 177 | | inss2 4238 |
. . . . . . . . . . 11
⊢
(((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ 𝐴 |
| 178 | 13 | uniiccdif 25613 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹) ∧
(vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹))) =
0)) |
| 179 | 178 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹)) |
| 180 | | ovolficcss 25504 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐹) ⊆
ℝ) |
| 181 | 13, 180 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) |
| 182 | 179, 181 | sstrd 3994 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) |
| 183 | 16, 182 | eqsstrid 4022 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 184 | 183 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐴 ⊆ ℝ) |
| 185 | 177, 184 | sstrid 3995 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ) |
| 186 | | inss1 4237 |
. . . . . . . . . . 11
⊢
(((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗)) |
| 187 | | ioossre 13448 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ⊆ ℝ |
| 188 | 167, 187 | eqsstrdi 4028 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
| 189 | 167 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) = (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗))))) |
| 190 | | ovolfcl 25501 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐺‘𝑗)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑗)) ≤ (2nd
‘(𝐺‘𝑗)))) |
| 191 | 6, 90, 190 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
| 192 | | ovolioo 25603 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗))) → (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗)))) = ((2nd
‘(𝐺‘𝑗)) − (1st
‘(𝐺‘𝑗)))) |
| 193 | 191, 192 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗)))) = ((2nd
‘(𝐺‘𝑗)) − (1st
‘(𝐺‘𝑗)))) |
| 194 | 189, 193 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
| 195 | 191 | simp2d 1144 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
| 196 | 191 | simp1d 1143 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
| 197 | 195, 196 | resubcld 11691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
| 198 | 194, 197 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) |
| 199 | | ovolsscl 25521 |
. . . . . . . . . . 11
⊢
(((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) →
(vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ) |
| 200 | 186, 188,
198, 199 | mp3an2i 1468 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ) |
| 201 | | mblsplit 25567 |
. . . . . . . . . 10
⊢
(((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol ∧ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ ∧
(vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ) →
(vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))))) |
| 202 | 176, 185,
200, 201 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))))) |
| 203 | | imassrn 6089 |
. . . . . . . . . . . . . . 15
⊢ (((,)
∘ 𝐹) “
(1...𝑁)) ⊆ ran ((,)
∘ 𝐹) |
| 204 | 203 | unissi 4916 |
. . . . . . . . . . . . . 14
⊢ ∪ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ∪ ran
((,) ∘ 𝐹) |
| 205 | 204, 69, 16 | 3sstr4i 4035 |
. . . . . . . . . . . . 13
⊢ 𝐿 ⊆ 𝐴 |
| 206 | | sslin 4243 |
. . . . . . . . . . . . 13
⊢ (𝐿 ⊆ 𝐴 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴)) |
| 207 | 205, 206 | mp1i 13 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴)) |
| 208 | | sseqin2 4223 |
. . . . . . . . . . . 12
⊢
((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ↔ ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) |
| 209 | 207, 208 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) |
| 210 | 209 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿))) |
| 211 | | indifdir 4295 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗)))) |
| 212 | | incom 4209 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐴) |
| 213 | | incom 4209 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿) |
| 214 | 212, 213 | difeq12i 4124 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗)))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) |
| 215 | 211, 214 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) |
| 216 | 79 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴) |
| 217 | 77 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐿 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
| 218 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑖 → ((,)‘(𝐹‘𝑥)) = ((,)‘(𝐹‘𝑖))) |
| 219 | 218 | cbvdisjv 5121 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Disj 𝑥
∈ ℕ ((,)‘(𝐹‘𝑥)) ↔ Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖))) |
| 220 | 14, 219 | sylib 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Disj 𝑖 ∈ ℕ
((,)‘(𝐹‘𝑖))) |
| 221 | | fz1ssnn 13595 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...𝑁) ⊆
ℕ |
| 222 | 221 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) |
| 223 | | uzss 12901 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 + 1) ∈
(ℤ≥‘1) → (ℤ≥‘(𝑁 + 1)) ⊆
(ℤ≥‘1)) |
| 224 | 39, 223 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆
(ℤ≥‘1)) |
| 225 | 224, 36 | sseqtrrdi 4025 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆ ℕ) |
| 226 | 47 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∩
(ℤ≥‘(𝑁 + 1))) = ((1...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) |
| 227 | | uzdisj 13637 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1...((𝑁 + 1)
− 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ |
| 228 | 226, 227 | eqtr3di 2792 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) =
∅) |
| 229 | | disjiun 5131 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Disj 𝑖
∈ ℕ ((,)‘(𝐹‘𝑖)) ∧ ((1...𝑁) ⊆ ℕ ∧
(ℤ≥‘(𝑁 + 1)) ⊆ ℕ ∧ ((1...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅)) → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) |
| 230 | 220, 222,
225, 228, 229 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) |
| 231 | 217, 230 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐿 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) |
| 232 | | uneqdifeq 4493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ⊆ 𝐴 ∧ (𝐿 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) → ((𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
| 233 | 205, 231,
232 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
| 234 | 216, 233 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∖ 𝐿) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
| 235 | 234 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐴 ∖ 𝐿) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
| 236 | 235 | ineq2d 4220 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
| 237 | | incom 4209 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿)) |
| 238 | 101, 98 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
| 239 | 236, 237,
238 | 3eqtr4g 2802 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 240 | 215, 239 | eqtr3id 2791 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 241 | 240 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 242 | 210, 241 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))) = ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
| 243 | 202, 242 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
| 244 | 200, 140 | resubcld 11691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ∈ ℝ) |
| 245 | | inss2 4238 |
. . . . . . . . . . . . 13
⊢
(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) |
| 246 | 188 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
| 247 | 198 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) |
| 248 | | ovolsscl 25521 |
. . . . . . . . . . . . 13
⊢
(((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) →
(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 249 | 245, 246,
247, 248 | mp3an2i 1468 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 250 | 148, 249 | fsumrecl 15770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 251 | | uniioombl.n2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀)) |
| 252 | 251 | r19.21bi 3251 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀)) |
| 253 | 250, 200,
140 | absdifltd 15472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀) ↔ (((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) < ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀))))) |
| 254 | 252, 253 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) < ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀)))) |
| 255 | 254 | simpld 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 256 | 244, 250,
255 | ltled 11409 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 257 | 147 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 258 | | mblvol 25565 |
. . . . . . . . . . . . . . . . 17
⊢
((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol →
(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 259 | 172, 258 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 260 | 259, 249 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 261 | 172, 260 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧
(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) |
| 262 | 261 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧
(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) |
| 263 | | inss1 4237 |
. . . . . . . . . . . . . . . 16
⊢
(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖)) |
| 264 | 263 | rgenw 3065 |
. . . . . . . . . . . . . . 15
⊢
∀𝑖 ∈
ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖)) |
| 265 | 220 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖))) |
| 266 | | disjss2 5113 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖)) → (Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 267 | 264, 265,
266 | mpsyl 68 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 268 | | disjss1 5116 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ⊆
ℕ → (Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 269 | 221, 267,
268 | mpsyl 68 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 270 | | volfiniun 25582 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∈ Fin
∧ ∀𝑖 ∈
(1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧
(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) ∧ Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 271 | 148, 262,
269, 270 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 272 | | mblvol 25565 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 273 | 175, 272 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 274 | 259 | sumeq2dv 15738 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 275 | 271, 273,
274 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 276 | 257, 275 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 277 | 256, 276 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿))) |
| 278 | 276, 250 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ∈ ℝ) |
| 279 | 200, 140,
278 | lesubaddd 11860 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ↔ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))) |
| 280 | 277, 279 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))) |
| 281 | 243, 280 | eqbrtrrd 5167 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))) |
| 282 | 131, 140,
278 | leadd2d 11858 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀) ↔ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))) |
| 283 | 281, 282 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀)) |
| 284 | 124, 131,
140, 283 | fsumle 15835 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀)) |
| 285 | 139 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℂ) |
| 286 | | fsumconst 15826 |
. . . . . . 7
⊢
(((1...𝑀) ∈ Fin
∧ (𝐶 / 𝑀) ∈ ℂ) →
Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀))) |
| 287 | 124, 285,
286 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀))) |
| 288 | | nnnn0 12533 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
| 289 | | hashfz1 14385 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
| 290 | 138, 288,
289 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) |
| 291 | 290 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((♯‘(1...𝑀)) · (𝐶 / 𝑀)) = (𝑀 · (𝐶 / 𝑀))) |
| 292 | 116 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 293 | 138 | nncnd 12282 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 294 | 138 | nnne0d 12316 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ≠ 0) |
| 295 | 292, 293,
294 | divcan2d 12045 |
. . . . . 6
⊢ (𝜑 → (𝑀 · (𝐶 / 𝑀)) = 𝐶) |
| 296 | 287, 291,
295 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = 𝐶) |
| 297 | 284, 296 | breqtrd 5169 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶) |
| 298 | 114, 132,
116, 137, 297 | letrd 11418 |
. . 3
⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶) |
| 299 | 114, 116,
34, 298 | leadd2dd 11878 |
. 2
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶)) |
| 300 | 31, 115, 117, 123, 299 | letrd 11418 |
1
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶)) |