Proof of Theorem uniioombllem4
Step | Hyp | Ref
| Expression |
1 | | inss1 3833 |
. . . 4
⊢ (𝐾 ∩ 𝐴) ⊆ 𝐾 |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ 𝐾) |
3 | | uniioombl.k |
. . . . . 6
⊢ 𝐾 = ∪
(((,) ∘ 𝐺) “
(1...𝑀)) |
4 | | imassrn 5477 |
. . . . . . 7
⊢ (((,)
∘ 𝐺) “
(1...𝑀)) ⊆ ran ((,)
∘ 𝐺) |
5 | 4 | unissi 4461 |
. . . . . 6
⊢ ∪ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ∪ ran
((,) ∘ 𝐺) |
6 | 3, 5 | eqsstri 3635 |
. . . . 5
⊢ 𝐾 ⊆ ∪ ran ((,) ∘ 𝐺) |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐾 ⊆ ∪ ran
((,) ∘ 𝐺)) |
8 | | uniioombl.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
9 | 8 | uniiccdif 23346 |
. . . . . 6
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺) ∧
(vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran
((,) ∘ 𝐺))) =
0)) |
10 | 9 | simpld 475 |
. . . . 5
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
([,] ∘ 𝐺)) |
11 | | ovolficcss 23238 |
. . . . . 6
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐺) ⊆
ℝ) |
12 | 8, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ) |
13 | 10, 12 | sstrd 3613 |
. . . 4
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ) |
14 | 7, 13 | sstrd 3613 |
. . 3
⊢ (𝜑 → 𝐾 ⊆ ℝ) |
15 | | uniioombl.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
16 | | uniioombl.2 |
. . . . . 6
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
17 | | uniioombl.3 |
. . . . . 6
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
18 | | uniioombl.a |
. . . . . 6
⊢ 𝐴 = ∪
ran ((,) ∘ 𝐹) |
19 | | uniioombl.e |
. . . . . 6
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) |
20 | | uniioombl.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
21 | | uniioombl.s |
. . . . . 6
⊢ (𝜑 → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
22 | | uniioombl.t |
. . . . . 6
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
23 | | uniioombl.v |
. . . . . 6
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐸) + 𝐶)) |
24 | 15, 16, 17, 18, 19, 20, 8, 21, 22, 23 | uniioombllem1 23349 |
. . . . 5
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
25 | | ssid 3624 |
. . . . . 6
⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran
((,) ∘ 𝐺) |
26 | 22 | ovollb 23247 |
. . . . . 6
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ((,) ∘
𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
27 | 8, 25, 26 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, <
)) |
28 | | ovollecl 23251 |
. . . . 5
⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < )
∈ ℝ ∧ (vol*‘∪ ran ((,) ∘
𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
→ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈
ℝ) |
29 | 13, 24, 27, 28 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) |
30 | | ovolsscl 23254 |
. . . 4
⊢ ((𝐾 ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran
((,) ∘ 𝐺) ⊆
ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) →
(vol*‘𝐾) ∈
ℝ) |
31 | 7, 13, 29, 30 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (vol*‘𝐾) ∈
ℝ) |
32 | | ovolsscl 23254 |
. . 3
⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∩ 𝐴)) ∈
ℝ) |
33 | 2, 14, 31, 32 | syl3anc 1326 |
. 2
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) |
34 | | inss1 3833 |
. . . . 5
⊢ (𝐾 ∩ 𝐿) ⊆ 𝐾 |
35 | 34 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ 𝐾) |
36 | | ovolsscl 23254 |
. . . 4
⊢ (((𝐾 ∩ 𝐿) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘(𝐾 ∩ 𝐿)) ∈
ℝ) |
37 | 35, 14, 31, 36 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐿)) ∈ ℝ) |
38 | | ssun2 3777 |
. . . . . 6
⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((𝐾 ∩ 𝐿) ∪ ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
39 | | nnuz 11723 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
40 | | uniioombl.n |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℕ) |
41 | 40 | peano2nnd 11037 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 + 1) ∈ ℕ) |
42 | 41, 39 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘1)) |
43 | | uzsplit 12412 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 + 1) ∈
(ℤ≥‘1) → (ℤ≥‘1) =
((1...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(ℤ≥‘1) = ((1...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1)))) |
45 | 39, 44 | syl5eq 2668 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ = ((1...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1)))) |
46 | 40 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℂ) |
47 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
48 | | pncan 10287 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
49 | 46, 47, 48 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
50 | 49 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...((𝑁 + 1) − 1)) = (1...𝑁)) |
51 | 50 | uneq1d 3766 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1))) = ((1...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) |
52 | 45, 51 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℕ = ((1...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))) |
53 | 52 | iuneq1d 4545 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = ∪
𝑖 ∈ ((1...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖))) |
54 | | iunxun 4605 |
. . . . . . . . . . 11
⊢ ∪ 𝑖 ∈ ((1...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖)) = (∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
55 | 53, 54 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = (∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
56 | | ioof 12271 |
. . . . . . . . . . . . . 14
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
57 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
58 | | rexpssxrxp 10084 |
. . . . . . . . . . . . . . . 16
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
59 | 57, 58 | sstri 3612 |
. . . . . . . . . . . . . . 15
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
60 | | fss 6056 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
61 | 15, 59, 60 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
62 | | fco 6058 |
. . . . . . . . . . . . . 14
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
63 | 56, 61, 62 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
64 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
((,) ∘ 𝐹) Fn
ℕ) |
65 | | fniunfv 6505 |
. . . . . . . . . . . . 13
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,)
∘ 𝐹)) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,)
∘ 𝐹)) |
67 | | fvco3 6275 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖))) |
68 | 15, 67 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖))) |
69 | 68 | iuneq2dv 4542 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ ℕ
((,)‘(𝐹‘𝑖))) |
70 | 66, 69 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪
𝑖 ∈ ℕ
((,)‘(𝐹‘𝑖))) |
71 | 18, 70 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = ∪ 𝑖 ∈ ℕ
((,)‘(𝐹‘𝑖))) |
72 | | uniioombl.l |
. . . . . . . . . . . 12
⊢ 𝐿 = ∪
(((,) ∘ 𝐹) “
(1...𝑁)) |
73 | | ffun 6048 |
. . . . . . . . . . . . . 14
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
Fun ((,) ∘ 𝐹)) |
74 | | funiunfv 6506 |
. . . . . . . . . . . . . 14
⊢ (Fun ((,)
∘ 𝐹) → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,)
∘ 𝐹) “
(1...𝑁))) |
75 | 63, 73, 74 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,)
∘ 𝐹) “
(1...𝑁))) |
76 | | elfznn 12370 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ) |
77 | 15, 76, 67 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖))) |
78 | 77 | iuneq2dv 4542 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))) |
79 | 75, 78 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ (((,) ∘ 𝐹) “ (1...𝑁)) = ∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))) |
80 | 72, 79 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))) |
81 | 80 | uneq1d 3766 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
82 | 55, 71, 81 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
83 | 82 | ineq2d 3814 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∩ 𝐴) = (𝐾 ∩ (𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))) |
84 | | indi 3873 |
. . . . . . . 8
⊢ (𝐾 ∩ (𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
85 | 83, 84 | syl6eq 2672 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))) |
86 | | fss 6056 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
87 | 8, 59, 86 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
88 | | fco 6058 |
. . . . . . . . . . . . . 14
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐺:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
89 | 56, 87, 88 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
90 | | ffun 6048 |
. . . . . . . . . . . . 13
⊢ (((,)
∘ 𝐺):ℕ⟶𝒫 ℝ →
Fun ((,) ∘ 𝐺)) |
91 | | funiunfv 6506 |
. . . . . . . . . . . . 13
⊢ (Fun ((,)
∘ 𝐺) → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,)
∘ 𝐺) “
(1...𝑀))) |
92 | 89, 90, 91 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,)
∘ 𝐺) “
(1...𝑀))) |
93 | | elfznn 12370 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
94 | | fvco3 6275 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗))) |
95 | 8, 93, 94 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗))) |
96 | 95 | iuneq2dv 4542 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
97 | 92, 96 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (1...𝑀)) = ∪
𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
98 | 3, 97 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
99 | 98 | ineq2d 3814 |
. . . . . . . . 9
⊢ (𝜑 → (∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾) = (∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪
𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))) |
100 | | incom 3805 |
. . . . . . . . 9
⊢ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾) |
101 | | iunin2 4584 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
102 | | incom 3805 |
. . . . . . . . . . . . . . 15
⊢
(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈
(ℤ≥‘(𝑁 + 1)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))) |
104 | 103 | iuneq2i 4539 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) |
105 | | incom 3805 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
106 | 101, 104,
105 | 3eqtr4ri 2655 |
. . . . . . . . . . . 12
⊢ (∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) |
107 | 106 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → (∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
108 | 107 | iuneq2i 4539 |
. . . . . . . . . 10
⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) |
109 | | iunin2 4584 |
. . . . . . . . . 10
⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪
𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
110 | 108, 109 | eqtr3i 2646 |
. . . . . . . . 9
⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪
𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
111 | 99, 100, 110 | 3eqtr4g 2681 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
112 | 111 | uneq2d 3767 |
. . . . . . 7
⊢ (𝜑 → ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
113 | 85, 112 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
114 | 38, 113 | syl5sseqr 3654 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ (𝐾 ∩ 𝐴)) |
115 | 114, 1 | syl6ss 3615 |
. . . 4
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾) |
116 | | ovolsscl 23254 |
. . . 4
⊢
((∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
117 | 115, 14, 31, 116 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
118 | 37, 117 | readdcld 10069 |
. 2
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ∈ ℝ) |
119 | 20 | rpred 11872 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℝ) |
120 | 37, 119 | readdcld 10069 |
. 2
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶) ∈ ℝ) |
121 | 113 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) = (vol*‘((𝐾 ∩ 𝐿) ∪ ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
122 | 35, 14 | sstrd 3613 |
. . . 4
⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ ℝ) |
123 | 115, 14 | sstrd 3613 |
. . . 4
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ) |
124 | | ovolun 23267 |
. . . 4
⊢ ((((𝐾 ∩ 𝐿) ⊆ ℝ ∧ (vol*‘(𝐾 ∩ 𝐿)) ∈ ℝ) ∧ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧
(vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) →
(vol*‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
125 | 122, 37, 123, 117, 124 | syl22anc 1327 |
. . 3
⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐿) ∪ ∪
𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
126 | 121, 125 | eqbrtrd 4675 |
. 2
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
127 | | fzfid 12772 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
128 | | iunss 4561 |
. . . . . . . 8
⊢ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ↔ ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾) |
129 | 115, 128 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾) |
130 | 129 | r19.21bi 2932 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾) |
131 | 14 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐾 ⊆ ℝ) |
132 | 31 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘𝐾) ∈ ℝ) |
133 | | ovolsscl 23254 |
. . . . . 6
⊢
((∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) →
(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
134 | 130, 131,
132, 133 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
135 | 127, 134 | fsumrecl 14465 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
136 | 130, 131 | sstrd 3613 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ) |
137 | 136, 134 | jca 554 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧
(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) |
138 | 137 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧
(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) |
139 | | ovolfiniun 23269 |
. . . . 5
⊢
(((1...𝑀) ∈ Fin
∧ ∀𝑗 ∈
(1...𝑀)(∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧
(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) →
(vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
140 | 127, 138,
139 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
141 | | uniioombl.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
142 | 119, 141 | nndivred 11069 |
. . . . . . 7
⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℝ) |
143 | 142 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶 / 𝑀) ∈ ℝ) |
144 | 80 | ineq2d 3814 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))) |
145 | 144 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))) |
146 | 102 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...𝑁) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))) |
147 | 146 | iuneq2i 4539 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) |
148 | | iunin2 4584 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))) |
149 | 147, 148 | eqtri 2644 |
. . . . . . . . . . . 12
⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))) |
150 | 145, 149 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = ∪
𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
151 | | fzfid 12772 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1...𝑁) ∈ Fin) |
152 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
153 | 15, 76, 152 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
154 | 57, 153 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ (ℝ ×
ℝ)) |
155 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑖) ∈ (ℝ × ℝ) →
(𝐹‘𝑖) = 〈(1st ‘(𝐹‘𝑖)), (2nd ‘(𝐹‘𝑖))〉) |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) = 〈(1st ‘(𝐹‘𝑖)), (2nd ‘(𝐹‘𝑖))〉) |
157 | 156 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((,)‘〈(1st
‘(𝐹‘𝑖)), (2nd
‘(𝐹‘𝑖))〉)) |
158 | | df-ov 6653 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(𝐹‘𝑖))(,)(2nd ‘(𝐹‘𝑖))) = ((,)‘〈(1st
‘(𝐹‘𝑖)), (2nd
‘(𝐹‘𝑖))〉) |
159 | 157, 158 | syl6eqr 2674 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((1st ‘(𝐹‘𝑖))(,)(2nd ‘(𝐹‘𝑖)))) |
160 | | ioombl 23333 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝐹‘𝑖))(,)(2nd ‘(𝐹‘𝑖))) ∈ dom vol |
161 | 159, 160 | syl6eqel 2709 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol) |
162 | 161 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol) |
163 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
164 | 8, 93, 163 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
165 | 57, 164 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ ×
ℝ)) |
166 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) →
(𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
167 | 165, 166 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
168 | 167 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉)) |
169 | | df-ov 6653 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉) |
170 | 168, 169 | syl6eqr 2674 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗)))) |
171 | | ioombl 23333 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ∈ dom vol |
172 | 170, 171 | syl6eqel 2709 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol) |
173 | 172 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol) |
174 | | inmbl 23310 |
. . . . . . . . . . . . . 14
⊢
((((,)‘(𝐹‘𝑖)) ∈ dom vol ∧ ((,)‘(𝐺‘𝑗)) ∈ dom vol) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) |
175 | 162, 173,
174 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) |
176 | 175 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) |
177 | | finiunmbl 23312 |
. . . . . . . . . . . 12
⊢
(((1...𝑁) ∈ Fin
∧ ∀𝑖 ∈
(1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) |
178 | 151, 176,
177 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) |
179 | 150, 178 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol) |
180 | | inss2 3834 |
. . . . . . . . . . 11
⊢
(((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ 𝐴 |
181 | 15 | uniiccdif 23346 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹) ∧
(vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹))) =
0)) |
182 | 181 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹)) |
183 | | ovolficcss 23238 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐹) ⊆
ℝ) |
184 | 15, 183 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) |
185 | 182, 184 | sstrd 3613 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) |
186 | 18, 185 | syl5eqss 3649 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
187 | 186 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐴 ⊆ ℝ) |
188 | 180, 187 | syl5ss 3614 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ) |
189 | | inss1 3833 |
. . . . . . . . . . . 12
⊢
(((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗)) |
190 | 189 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗))) |
191 | | ioossre 12235 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ⊆ ℝ |
192 | 170, 191 | syl6eqss 3655 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
193 | 170 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) = (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗))))) |
194 | | ovolfcl 23235 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐺‘𝑗)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑗)) ≤ (2nd
‘(𝐺‘𝑗)))) |
195 | 8, 93, 194 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
196 | | ovolioo 23336 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗))) → (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗)))) = ((2nd
‘(𝐺‘𝑗)) − (1st
‘(𝐺‘𝑗)))) |
197 | 195, 196 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗)))) = ((2nd
‘(𝐺‘𝑗)) − (1st
‘(𝐺‘𝑗)))) |
198 | 193, 197 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
199 | 195 | simp2d 1074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
200 | 195 | simp1d 1073 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
201 | 199, 200 | resubcld 10458 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
202 | 198, 201 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) |
203 | | ovolsscl 23254 |
. . . . . . . . . . 11
⊢
(((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) →
(vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ) |
204 | 190, 192,
202, 203 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ) |
205 | | mblsplit 23300 |
. . . . . . . . . 10
⊢
(((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol ∧ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ ∧
(vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ) →
(vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))))) |
206 | 179, 188,
204, 205 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))))) |
207 | | imassrn 5477 |
. . . . . . . . . . . . . . 15
⊢ (((,)
∘ 𝐹) “
(1...𝑁)) ⊆ ran ((,)
∘ 𝐹) |
208 | 207 | unissi 4461 |
. . . . . . . . . . . . . 14
⊢ ∪ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ∪ ran
((,) ∘ 𝐹) |
209 | 208, 72, 18 | 3sstr4i 3644 |
. . . . . . . . . . . . 13
⊢ 𝐿 ⊆ 𝐴 |
210 | | sslin 3839 |
. . . . . . . . . . . . 13
⊢ (𝐿 ⊆ 𝐴 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴)) |
211 | 209, 210 | mp1i 13 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴)) |
212 | | sseqin2 3817 |
. . . . . . . . . . . 12
⊢
((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ↔ ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) |
213 | 211, 212 | sylib 208 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) |
214 | 213 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿))) |
215 | | indifdir 3883 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗)))) |
216 | | incom 3805 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐴) |
217 | | incom 3805 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿) |
218 | 216, 217 | difeq12i 3726 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗)))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) |
219 | 215, 218 | eqtri 2644 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) |
220 | 82 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴) |
221 | 80 | ineq1d 3813 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐿 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪
𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
222 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑖 → (𝐹‘𝑥) = (𝐹‘𝑖)) |
223 | 222 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑖 → ((,)‘(𝐹‘𝑥)) = ((,)‘(𝐹‘𝑖))) |
224 | 223 | cbvdisjv 4631 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Disj 𝑥
∈ ℕ ((,)‘(𝐹‘𝑥)) ↔ Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖))) |
225 | 16, 224 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Disj 𝑖 ∈ ℕ
((,)‘(𝐹‘𝑖))) |
226 | 76 | ssriv 3607 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...𝑁) ⊆
ℕ |
227 | 226 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) |
228 | | uzss 11708 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 + 1) ∈
(ℤ≥‘1) → (ℤ≥‘(𝑁 + 1)) ⊆
(ℤ≥‘1)) |
229 | 42, 228 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆
(ℤ≥‘1)) |
230 | 229, 39 | syl6sseqr 3652 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆ ℕ) |
231 | | uzdisj 12413 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1...((𝑁 + 1)
− 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ |
232 | 50 | ineq1d 3813 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∩
(ℤ≥‘(𝑁 + 1))) = ((1...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) |
233 | 231, 232 | syl5reqr 2671 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) =
∅) |
234 | | disjiun 4640 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Disj 𝑖
∈ ℕ ((,)‘(𝐹‘𝑖)) ∧ ((1...𝑁) ⊆ ℕ ∧
(ℤ≥‘(𝑁 + 1)) ⊆ ℕ ∧ ((1...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅)) → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) |
235 | 225, 227,
230, 233, 234 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) |
236 | 221, 235 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐿 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) |
237 | | uneqdifeq 4057 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ⊆ 𝐴 ∧ (𝐿 ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) → ((𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
238 | 209, 236,
237 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 ∪ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
239 | 220, 238 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∖ 𝐿) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
240 | 239 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐴 ∖ 𝐿) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
241 | 240 | ineq2d 3814 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) |
242 | | incom 3805 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿)) |
243 | 104, 101 | eqtri 2644 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) |
244 | 241, 242,
243 | 3eqtr4g 2681 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
245 | 219, 244 | syl5eqr 2670 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = ∪
𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
246 | 245 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
247 | 214, 246 | oveq12d 6668 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))) = ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
248 | 206, 247 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))) |
249 | 204, 143 | resubcld 10458 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ∈ ℝ) |
250 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢
(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) |
251 | 250 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗))) |
252 | 192 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
253 | 202 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) |
254 | | ovolsscl 23254 |
. . . . . . . . . . . . 13
⊢
(((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) →
(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
255 | 251, 252,
253, 254 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
256 | 151, 255 | fsumrecl 14465 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
257 | | uniioombl.n2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀)) |
258 | 257 | r19.21bi 2932 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀)) |
259 | 256, 204,
143 | absdifltd 14172 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀) ↔ (((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) < ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀))))) |
260 | 258, 259 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) < ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀)))) |
261 | 260 | simpld 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
262 | 249, 256,
261 | ltled 10185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
263 | 150 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
264 | | mblvol 23298 |
. . . . . . . . . . . . . . . . 17
⊢
((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol →
(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
265 | 175, 264 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
266 | 265, 255 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
267 | 175, 266 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧
(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) |
268 | 267 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧
(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) |
269 | | inss1 3833 |
. . . . . . . . . . . . . . . 16
⊢
(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖)) |
270 | 269 | rgenw 2924 |
. . . . . . . . . . . . . . 15
⊢
∀𝑖 ∈
ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖)) |
271 | 225 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖))) |
272 | | disjss2 4623 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖)) → (Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
273 | 270, 271,
272 | mpsyl 68 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
274 | | disjss1 4626 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ⊆
ℕ → (Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
275 | 226, 273,
274 | mpsyl 68 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
276 | | volfiniun 23315 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∈ Fin
∧ ∀𝑖 ∈
(1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧
(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) ∧ Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
277 | 151, 268,
275, 276 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
278 | | mblvol 23298 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
279 | 178, 278 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
280 | 265 | sumeq2dv 14433 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
281 | 277, 279,
280 | 3eqtr3d 2664 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
282 | 263, 281 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
283 | 262, 282 | breqtrrd 4681 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿))) |
284 | 282, 256 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ∈ ℝ) |
285 | 204, 143,
284 | lesubaddd 10624 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ↔ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))) |
286 | 283, 285 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))) |
287 | 248, 286 | eqbrtrrd 4677 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))) |
288 | 134, 143,
284 | leadd2d 10622 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀) ↔ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))) |
289 | 287, 288 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀)) |
290 | 127, 134,
143, 289 | fsumle 14531 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀)) |
291 | 142 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℂ) |
292 | | fsumconst 14522 |
. . . . . . 7
⊢
(((1...𝑀) ∈ Fin
∧ (𝐶 / 𝑀) ∈ ℂ) →
Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((#‘(1...𝑀)) · (𝐶 / 𝑀))) |
293 | 127, 291,
292 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((#‘(1...𝑀)) · (𝐶 / 𝑀))) |
294 | | nnnn0 11299 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
295 | | hashfz1 13134 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (#‘(1...𝑀)) =
𝑀) |
296 | 141, 294,
295 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (#‘(1...𝑀)) = 𝑀) |
297 | 296 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → ((#‘(1...𝑀)) · (𝐶 / 𝑀)) = (𝑀 · (𝐶 / 𝑀))) |
298 | 119 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
299 | 141 | nncnd 11036 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
300 | 141 | nnne0d 11065 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ≠ 0) |
301 | 298, 299,
300 | divcan2d 10803 |
. . . . . 6
⊢ (𝜑 → (𝑀 · (𝐶 / 𝑀)) = 𝐶) |
302 | 293, 297,
301 | 3eqtrd 2660 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = 𝐶) |
303 | 290, 302 | breqtrd 4679 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶) |
304 | 117, 135,
119, 140, 303 | letrd 10194 |
. . 3
⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶) |
305 | 117, 119,
37, 304 | leadd2dd 10642 |
. 2
⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈
(ℤ≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶)) |
306 | 33, 118, 120, 126, 305 | letrd 10194 |
1
⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶)) |