Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11408 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | uniioombl.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
4 | | eqidd 2623 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) = (𝑇‘𝑚)) |
5 | | uniioombl.t |
. . . . . 6
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
6 | | eqidd 2623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑎) = (((abs ∘ − ) ∘ 𝐺)‘𝑎)) |
7 | | uniioombl.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
8 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
9 | 8 | ovolfsf 23240 |
. . . . . . . . . 10
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞)) |
10 | 7, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐺):ℕ⟶(0[,)+∞)) |
11 | 10 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑎) ∈ (0[,)+∞)) |
12 | | elrege0 12278 |
. . . . . . . 8
⊢ ((((abs
∘ − ) ∘ 𝐺)‘𝑎) ∈ (0[,)+∞) ↔ ((((abs
∘ − ) ∘ 𝐺)‘𝑎) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐺)‘𝑎))) |
13 | 11, 12 | sylib 208 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → ((((abs ∘
− ) ∘ 𝐺)‘𝑎) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐺)‘𝑎))) |
14 | 13 | simpld 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑎) ∈ ℝ) |
15 | 13 | simprd 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → 0 ≤ (((abs ∘
− ) ∘ 𝐺)‘𝑎)) |
16 | | uniioombl.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
17 | | uniioombl.2 |
. . . . . . . 8
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
18 | | uniioombl.3 |
. . . . . . . 8
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
19 | | uniioombl.a |
. . . . . . . 8
⊢ 𝐴 = ∪
ran ((,) ∘ 𝐹) |
20 | | uniioombl.e |
. . . . . . . 8
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) |
21 | | uniioombl.s |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
22 | | uniioombl.v |
. . . . . . . 8
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐸) + 𝐶)) |
23 | 16, 17, 18, 19, 20, 3, 7, 21, 5,
22 | uniioombllem1 23349 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
24 | 8, 5 | ovolsf 23241 |
. . . . . . . . . . . . 13
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞)) |
25 | 7, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞)) |
26 | | frn 6053 |
. . . . . . . . . . . 12
⊢ (𝑇:ℕ⟶(0[,)+∞)
→ ran 𝑇 ⊆
(0[,)+∞)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞)) |
28 | | icossxr 12258 |
. . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ ℝ* |
29 | 27, 28 | syl6ss 3615 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
30 | | supxrub 12154 |
. . . . . . . . . 10
⊢ ((ran
𝑇 ⊆
ℝ* ∧ 𝑥
∈ ran 𝑇) → 𝑥 ≤ sup(ran 𝑇, ℝ*, <
)) |
31 | 29, 30 | sylan 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝑇) → 𝑥 ≤ sup(ran 𝑇, ℝ*, <
)) |
32 | 31 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, <
)) |
33 | | ffn 6045 |
. . . . . . . . . 10
⊢ (𝑇:ℕ⟶(0[,)+∞)
→ 𝑇 Fn
ℕ) |
34 | 25, 33 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 Fn ℕ) |
35 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑇‘𝑚) → (𝑥 ≤ sup(ran 𝑇, ℝ*, < ) ↔ (𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, <
))) |
36 | 35 | ralrn 6362 |
. . . . . . . . 9
⊢ (𝑇 Fn ℕ →
(∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < ) ↔
∀𝑚 ∈ ℕ
(𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, <
))) |
37 | 34, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < ) ↔
∀𝑚 ∈ ℕ
(𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, <
))) |
38 | 32, 37 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → ∀𝑚 ∈ ℕ (𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, <
)) |
39 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑥 = sup(ran 𝑇, ℝ*, < ) → ((𝑇‘𝑚) ≤ 𝑥 ↔ (𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, <
))) |
40 | 39 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑥 = sup(ran 𝑇, ℝ*, < ) →
(∀𝑚 ∈ ℕ
(𝑇‘𝑚) ≤ 𝑥 ↔ ∀𝑚 ∈ ℕ (𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, <
))) |
41 | 40 | rspcev 3309 |
. . . . . . 7
⊢ ((sup(ran
𝑇, ℝ*,
< ) ∈ ℝ ∧ ∀𝑚 ∈ ℕ (𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, < )) →
∃𝑥 ∈ ℝ
∀𝑚 ∈ ℕ
(𝑇‘𝑚) ≤ 𝑥) |
42 | 23, 38, 41 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ ℕ (𝑇‘𝑚) ≤ 𝑥) |
43 | 1, 5, 2, 6, 14, 15, 42 | isumsup2 14578 |
. . . . 5
⊢ (𝜑 → 𝑇 ⇝ sup(ran 𝑇, ℝ, < )) |
44 | | rge0ssre 12280 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
45 | 27, 44 | syl6ss 3615 |
. . . . . 6
⊢ (𝜑 → ran 𝑇 ⊆ ℝ) |
46 | | 1nn 11031 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
47 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝑇:ℕ⟶(0[,)+∞)
→ dom 𝑇 =
ℕ) |
48 | 25, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑇 = ℕ) |
49 | 46, 48 | syl5eleqr 2708 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈ dom 𝑇) |
50 | | ne0i 3921 |
. . . . . . . 8
⊢ (1 ∈
dom 𝑇 → dom 𝑇 ≠ ∅) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom 𝑇 ≠ ∅) |
52 | | dm0rn0 5342 |
. . . . . . . 8
⊢ (dom
𝑇 = ∅ ↔ ran
𝑇 =
∅) |
53 | 52 | necon3bii 2846 |
. . . . . . 7
⊢ (dom
𝑇 ≠ ∅ ↔ ran
𝑇 ≠
∅) |
54 | 51, 53 | sylib 208 |
. . . . . 6
⊢ (𝜑 → ran 𝑇 ≠ ∅) |
55 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑦 = sup(ran 𝑇, ℝ*, < ) → (𝑥 ≤ 𝑦 ↔ 𝑥 ≤ sup(ran 𝑇, ℝ*, <
))) |
56 | 55 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑦 = sup(ran 𝑇, ℝ*, < ) →
(∀𝑥 ∈ ran 𝑇 𝑥 ≤ 𝑦 ↔ ∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, <
))) |
57 | 56 | rspcev 3309 |
. . . . . . 7
⊢ ((sup(ran
𝑇, ℝ*,
< ) ∈ ℝ ∧ ∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < )) →
∃𝑦 ∈ ℝ
∀𝑥 ∈ ran 𝑇 𝑥 ≤ 𝑦) |
58 | 23, 32, 57 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ran 𝑇 𝑥 ≤ 𝑦) |
59 | | supxrre 12157 |
. . . . . 6
⊢ ((ran
𝑇 ⊆ ℝ ∧ ran
𝑇 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑥 ∈ ran 𝑇 𝑥 ≤ 𝑦) → sup(ran 𝑇, ℝ*, < ) = sup(ran
𝑇, ℝ, <
)) |
60 | 45, 54, 58, 59 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran
𝑇, ℝ, <
)) |
61 | 43, 60 | breqtrrd 4681 |
. . . 4
⊢ (𝜑 → 𝑇 ⇝ sup(ran 𝑇, ℝ*, <
)) |
62 | 1, 2, 3, 4, 61 | climi2 14242 |
. . 3
⊢ (𝜑 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) |
63 | 1 | r19.2uz 14091 |
. . 3
⊢
(∃𝑗 ∈
ℕ ∀𝑚 ∈
(ℤ≥‘𝑗)(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶 → ∃𝑚 ∈ ℕ
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶) |
64 | 62, 63 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ ℕ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) |
65 | | 1zzd 11408 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 1 ∈ ℤ) |
66 | 3 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 𝐶 ∈
ℝ+) |
67 | | simplrl 800 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 𝑚 ∈ ℕ) |
68 | 67 | nnrpd 11870 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 𝑚 ∈ ℝ+) |
69 | 66, 68 | rpdivcld 11889 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐶 / 𝑚) ∈
ℝ+) |
70 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
((,)‘(𝐹‘𝑧)) ∈ V |
71 | 70 | inex1 4799 |
. . . . . . . . . . . . . . 15
⊢
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) ∈ V |
72 | 71 | rgenw 2924 |
. . . . . . . . . . . . . 14
⊢
∀𝑧 ∈
ℕ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) ∈ V |
73 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) |
74 | 73 | fnmpt 6020 |
. . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
ℕ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) ∈ V → (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) Fn ℕ) |
75 | 72, 74 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) Fn ℕ) |
76 | | elfznn 12370 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...𝑛) → 𝑖 ∈ ℕ) |
77 | | fvco2 6273 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) Fn ℕ ∧ 𝑖 ∈ ℕ) → ((vol* ∘ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))‘𝑖) = (vol*‘((𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))‘𝑖))) |
78 | 75, 76, 77 | syl2an 494 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))‘𝑖) = (vol*‘((𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))‘𝑖))) |
79 | 76 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ ℕ) |
80 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑖 → (𝐹‘𝑧) = (𝐹‘𝑖)) |
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑖 → ((,)‘(𝐹‘𝑧)) = ((,)‘(𝐹‘𝑖))) |
82 | 81 | ineq1d 3813 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑖 → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
83 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
((,)‘(𝐹‘𝑖)) ∈ V |
84 | 83 | inex1 4799 |
. . . . . . . . . . . . . . 15
⊢
(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ V |
85 | 82, 73, 84 | fvmpt 6282 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ → ((𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))‘𝑖) = (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
86 | 79, 85 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))‘𝑖) = (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
87 | 86 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘((𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))‘𝑖)) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
88 | 78, 87 | eqtrd 2656 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))‘𝑖) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
89 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
90 | 89, 1 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
91 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢
(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) |
92 | 91 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗))) |
93 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . 19
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
94 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
95 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...𝑚) → 𝑗 ∈ ℕ) |
96 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
97 | 94, 95, 96 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
98 | 93, 97 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐺‘𝑗) ∈ (ℝ ×
ℝ)) |
99 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) →
(𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
101 | 100 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((,)‘(𝐺‘𝑗)) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉)) |
102 | | df-ov 6653 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉) |
103 | 101, 102 | syl6eqr 2674 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((,)‘(𝐺‘𝑗)) = ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗)))) |
104 | | ioossre 12235 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ⊆ ℝ |
105 | 103, 104 | syl6eqss 3655 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
106 | 105 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
107 | 103 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((,)‘(𝐺‘𝑗))) = (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗))))) |
108 | | ovolfcl 23235 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐺‘𝑗)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑗)) ≤ (2nd
‘(𝐺‘𝑗)))) |
109 | 94, 95, 108 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
110 | | ovolioo 23336 |
. . . . . . . . . . . . . . . . 17
⊢
(((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗))) → (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗)))) = ((2nd
‘(𝐺‘𝑗)) − (1st
‘(𝐺‘𝑗)))) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗)))) = ((2nd
‘(𝐺‘𝑗)) − (1st
‘(𝐺‘𝑗)))) |
112 | 107, 111 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((,)‘(𝐺‘𝑗))) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
113 | 109 | simp2d 1074 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
114 | 109 | simp1d 1073 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
115 | 113, 114 | resubcld 10458 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
116 | 112, 115 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) |
117 | 116 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) |
118 | | ovolsscl 23254 |
. . . . . . . . . . . . 13
⊢
(((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) →
(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
119 | 92, 106, 117, 118 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
120 | 119 | recnd 10068 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℂ) |
121 | 88, 90, 120 | fsumser 14461 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))))‘𝑛)) |
122 | 121 | eqcomd 2628 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → (seq1( + , (vol*
∘ (𝑧 ∈ ℕ
↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))))‘𝑛) = Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
123 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑘 → (𝐹‘𝑧) = (𝐹‘𝑘)) |
124 | 123 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑘 → ((,)‘(𝐹‘𝑧)) = ((,)‘(𝐹‘𝑘))) |
125 | 124 | ineq1d 3813 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑘 → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐹‘𝑘)) ∩ ((,)‘(𝐺‘𝑗)))) |
126 | 125 | cbvmptv 4750 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) = (𝑘 ∈ ℕ ↦ (((,)‘(𝐹‘𝑘)) ∩ ((,)‘(𝐺‘𝑗)))) |
127 | | eqeq1 2626 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑧 = ∅ ↔ 𝑥 = ∅)) |
128 | | infeq1 8382 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → inf(𝑧, ℝ*, < ) = inf(𝑥, ℝ*, <
)) |
129 | | supeq1 8351 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → sup(𝑧, ℝ*, < ) = sup(𝑥, ℝ*, <
)) |
130 | 128, 129 | opeq12d 4410 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → 〈inf(𝑧, ℝ*, < ), sup(𝑧, ℝ*, <
)〉 = 〈inf(𝑥,
ℝ*, < ), sup(𝑥, ℝ*, <
)〉) |
131 | 127, 130 | ifbieq2d 4111 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → if(𝑧 = ∅, 〈0, 0〉, 〈inf(𝑧, ℝ*, < ),
sup(𝑧, ℝ*,
< )〉) = if(𝑥 =
∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, <
)〉)) |
132 | 131 | cbvmptv 4750 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ran (,) ↦ if(𝑧 = ∅, 〈0, 0〉,
〈inf(𝑧,
ℝ*, < ), sup(𝑧, ℝ*, < )〉)) =
(𝑥 ∈ ran (,) ↦
if(𝑥 = ∅, 〈0,
0〉, 〈inf(𝑥,
ℝ*, < ), sup(𝑥, ℝ*, <
)〉)) |
133 | 16, 17, 18, 19, 20, 3, 7, 21, 5,
22, 126, 132 | uniioombllem2 23351 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → seq1( + , (vol*
∘ (𝑧 ∈ ℕ
↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))) ⇝ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴))) |
134 | 95, 133 | sylan2 491 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑚)) → seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))) ⇝ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴))) |
135 | 134 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))) ⇝ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴))) |
136 | 1, 65, 69, 122, 135 | climi2 14242 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ∃𝑎 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
137 | | 1z 11407 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
138 | 1 | rexuz3 14088 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → (∃𝑎
∈ ℕ ∀𝑛
∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))) |
139 | 137, 138 | ax-mp 5 |
. . . . . . . 8
⊢
(∃𝑎 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
140 | 136, 139 | sylib 208 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
141 | 140 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∀𝑗 ∈ (1...𝑚)∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
142 | | fzfi 12771 |
. . . . . . 7
⊢
(1...𝑚) ∈
Fin |
143 | | rexfiuz 14087 |
. . . . . . 7
⊢
((1...𝑚) ∈ Fin
→ (∃𝑎 ∈
ℤ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∀𝑗 ∈ (1...𝑚)∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))) |
144 | 142, 143 | ax-mp 5 |
. . . . . 6
⊢
(∃𝑎 ∈
ℤ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∀𝑗 ∈ (1...𝑚)∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
145 | 141, 144 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∃𝑎 ∈ ℤ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
146 | 1 | rexuz3 14088 |
. . . . . 6
⊢ (1 ∈
ℤ → (∃𝑎
∈ ℕ ∀𝑛
∈ (ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))) |
147 | 137, 146 | ax-mp 5 |
. . . . 5
⊢
(∃𝑎 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
148 | 145, 147 | sylibr 224 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∃𝑎 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
149 | 1 | r19.2uz 14091 |
. . . 4
⊢
(∃𝑎 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) → ∃𝑛 ∈ ℕ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
150 | 148, 149 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∃𝑛 ∈ ℕ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
151 | 16 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
152 | 17 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) |
153 | 20 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → (vol*‘𝐸) ∈ ℝ) |
154 | 3 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐶 ∈
ℝ+) |
155 | 7 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
156 | 21 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
157 | 22 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐸) + 𝐶)) |
158 | | simprll 802 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝑚 ∈ ℕ) |
159 | | simprlr 803 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) |
160 | | eqid 2622 |
. . . . 5
⊢ ∪ (((,) ∘ 𝐺) “ (1...𝑚)) = ∪ (((,)
∘ 𝐺) “
(1...𝑚)) |
161 | | simprrl 804 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝑛 ∈ ℕ) |
162 | | simprrr 805 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
163 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑧 → (𝐹‘𝑖) = (𝐹‘𝑧)) |
164 | 163 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑧 → ((,)‘(𝐹‘𝑖)) = ((,)‘(𝐹‘𝑧))) |
165 | 164 | ineq1d 3813 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑧 → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) |
166 | 165 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑧 → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))) |
167 | 166 | cbvsumv 14426 |
. . . . . . . . . . 11
⊢
Σ𝑖 ∈
(1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) |
168 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑘 → (𝐺‘𝑗) = (𝐺‘𝑘)) |
169 | 168 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑘 → ((,)‘(𝐺‘𝑗)) = ((,)‘(𝐺‘𝑘))) |
170 | 169 | ineq2d 3814 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) |
171 | 170 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘))))) |
172 | 171 | sumeq2sdv 14435 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘))))) |
173 | 167, 172 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘))))) |
174 | 169 | ineq1d 3813 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (((,)‘(𝐺‘𝑗)) ∩ 𝐴) = (((,)‘(𝐺‘𝑘)) ∩ 𝐴)) |
175 | 174 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴))) |
176 | 173, 175 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴))) = (Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) − (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴)))) |
177 | 176 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) = (abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) − (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴))))) |
178 | 177 | breq1d 4663 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ (abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) − (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴)))) < (𝐶 / 𝑚))) |
179 | 178 | cbvralv 3171 |
. . . . . 6
⊢
(∀𝑗 ∈
(1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∀𝑘 ∈ (1...𝑚)(abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) − (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
180 | 162, 179 | sylib 208 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → ∀𝑘 ∈ (1...𝑚)(abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) − (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
181 | | eqid 2622 |
. . . . 5
⊢ ∪ (((,) ∘ 𝐹) “ (1...𝑛)) = ∪ (((,)
∘ 𝐹) “
(1...𝑛)) |
182 | 151, 152,
18, 19, 153, 154, 155, 156, 5, 157, 158, 159, 160, 161, 180, 181 | uniioombllem5 23355 |
. . . 4
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) |
183 | 182 | anassrs 680 |
. . 3
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))) → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) |
184 | 150, 183 | rexlimddv 3035 |
. 2
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) |
185 | 64, 184 | rexlimddv 3035 |
1
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) |