| Step | Hyp | Ref
| Expression |
| 1 | | nnuz 12921 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
| 2 | | 1zzd 12648 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
| 3 | | uniioombl.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
| 4 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) = (𝑇‘𝑚)) |
| 5 | | uniioombl.t |
. . . . . 6
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
| 6 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑎) = (((abs ∘ − ) ∘ 𝐺)‘𝑎)) |
| 7 | | uniioombl.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 8 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
| 9 | 8 | ovolfsf 25506 |
. . . . . . . . . 10
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞)) |
| 10 | 7, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐺):ℕ⟶(0[,)+∞)) |
| 11 | 10 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑎) ∈ (0[,)+∞)) |
| 12 | | elrege0 13494 |
. . . . . . . 8
⊢ ((((abs
∘ − ) ∘ 𝐺)‘𝑎) ∈ (0[,)+∞) ↔ ((((abs
∘ − ) ∘ 𝐺)‘𝑎) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐺)‘𝑎))) |
| 13 | 11, 12 | sylib 218 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → ((((abs ∘
− ) ∘ 𝐺)‘𝑎) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐺)‘𝑎))) |
| 14 | 13 | simpld 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑎) ∈ ℝ) |
| 15 | 13 | simprd 495 |
. . . . . 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 25616 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
| 24 | 8, 5 | ovolsf 25507 |
. . . . . . . . . . . . 13
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞)) |
| 25 | 7, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞)) |
| 26 | 25 | frnd 6744 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞)) |
| 27 | | icossxr 13472 |
. . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ ℝ* |
| 28 | 26, 27 | sstrdi 3996 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
| 29 | | supxrub 13366 |
. . . . . . . . . 10
⊢ ((ran
𝑇 ⊆
ℝ* ∧ 𝑥
∈ ran 𝑇) → 𝑥 ≤ sup(ran 𝑇, ℝ*, <
)) |
| 30 | 28, 29 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝑇) → 𝑥 ≤ sup(ran 𝑇, ℝ*, <
)) |
| 31 | 30 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, <
)) |
| 32 | 25 | ffnd 6737 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 Fn ℕ) |
| 33 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑇‘𝑚) → (𝑥 ≤ sup(ran 𝑇, ℝ*, < ) ↔ (𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, <
))) |
| 34 | 33 | ralrn 7108 |
. . . . . . . . 9
⊢ (𝑇 Fn ℕ →
(∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < ) ↔
∀𝑚 ∈ ℕ
(𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, <
))) |
| 35 | 32, 34 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < ) ↔
∀𝑚 ∈ ℕ
(𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, <
))) |
| 36 | 31, 35 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → ∀𝑚 ∈ ℕ (𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, <
)) |
| 37 | | brralrspcev 5203 |
. . . . . . 7
⊢ ((sup(ran
𝑇, ℝ*,
< ) ∈ ℝ ∧ ∀𝑚 ∈ ℕ (𝑇‘𝑚) ≤ sup(ran 𝑇, ℝ*, < )) →
∃𝑥 ∈ ℝ
∀𝑚 ∈ ℕ
(𝑇‘𝑚) ≤ 𝑥) |
| 38 | 23, 36, 37 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ ℕ (𝑇‘𝑚) ≤ 𝑥) |
| 39 | 1, 5, 2, 6, 14, 15, 38 | isumsup2 15882 |
. . . . 5
⊢ (𝜑 → 𝑇 ⇝ sup(ran 𝑇, ℝ, < )) |
| 40 | | rge0ssre 13496 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
| 41 | 26, 40 | sstrdi 3996 |
. . . . . 6
⊢ (𝜑 → ran 𝑇 ⊆ ℝ) |
| 42 | | 1nn 12277 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
| 43 | 25 | fdmd 6746 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑇 = ℕ) |
| 44 | 42, 43 | eleqtrrid 2848 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈ dom 𝑇) |
| 45 | 44 | ne0d 4342 |
. . . . . . 7
⊢ (𝜑 → dom 𝑇 ≠ ∅) |
| 46 | | dm0rn0 5935 |
. . . . . . . 8
⊢ (dom
𝑇 = ∅ ↔ ran
𝑇 =
∅) |
| 47 | 46 | necon3bii 2993 |
. . . . . . 7
⊢ (dom
𝑇 ≠ ∅ ↔ ran
𝑇 ≠
∅) |
| 48 | 45, 47 | sylib 218 |
. . . . . 6
⊢ (𝜑 → ran 𝑇 ≠ ∅) |
| 49 | | brralrspcev 5203 |
. . . . . . 7
⊢ ((sup(ran
𝑇, ℝ*,
< ) ∈ ℝ ∧ ∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < )) →
∃𝑦 ∈ ℝ
∀𝑥 ∈ ran 𝑇 𝑥 ≤ 𝑦) |
| 50 | 23, 31, 49 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ran 𝑇 𝑥 ≤ 𝑦) |
| 51 | | supxrre 13369 |
. . . . . 6
⊢ ((ran
𝑇 ⊆ ℝ ∧ ran
𝑇 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑥 ∈ ran 𝑇 𝑥 ≤ 𝑦) → sup(ran 𝑇, ℝ*, < ) = sup(ran
𝑇, ℝ, <
)) |
| 52 | 41, 48, 50, 51 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran
𝑇, ℝ, <
)) |
| 53 | 39, 52 | breqtrrd 5171 |
. . . 4
⊢ (𝜑 → 𝑇 ⇝ sup(ran 𝑇, ℝ*, <
)) |
| 54 | 1, 2, 3, 4, 53 | climi2 15547 |
. . 3
⊢ (𝜑 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) |
| 55 | 1 | r19.2uz 15390 |
. . 3
⊢
(∃𝑗 ∈
ℕ ∀𝑚 ∈
(ℤ≥‘𝑗)(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶 → ∃𝑚 ∈ ℕ
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶) |
| 56 | 54, 55 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ ℕ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) |
| 57 | | 1zzd 12648 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 1 ∈ ℤ) |
| 58 | 3 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 𝐶 ∈
ℝ+) |
| 59 | | simplrl 777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 𝑚 ∈ ℕ) |
| 60 | 59 | nnrpd 13075 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 𝑚 ∈ ℝ+) |
| 61 | 58, 60 | rpdivcld 13094 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐶 / 𝑚) ∈
ℝ+) |
| 62 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢
((,)‘(𝐹‘𝑧)) ∈ V |
| 63 | 62 | inex1 5317 |
. . . . . . . . . . . . . . 15
⊢
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) ∈ V |
| 64 | 63 | rgenw 3065 |
. . . . . . . . . . . . . 14
⊢
∀𝑧 ∈
ℕ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) ∈ V |
| 65 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 66 | 65 | fnmpt 6708 |
. . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
ℕ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) ∈ V → (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) Fn ℕ) |
| 67 | 64, 66 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) Fn ℕ) |
| 68 | | elfznn 13593 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...𝑛) → 𝑖 ∈ ℕ) |
| 69 | | fvco2 7006 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) Fn ℕ ∧ 𝑖 ∈ ℕ) → ((vol* ∘ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))‘𝑖) = (vol*‘((𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))‘𝑖))) |
| 70 | 67, 68, 69 | syl2an 596 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))‘𝑖) = (vol*‘((𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))‘𝑖))) |
| 71 | 68 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ ℕ) |
| 72 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑖 → ((,)‘(𝐹‘𝑧)) = ((,)‘(𝐹‘𝑖))) |
| 73 | 72 | ineq1d 4219 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑖 → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 74 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢
((,)‘(𝐹‘𝑖)) ∈ V |
| 75 | 74 | inex1 5317 |
. . . . . . . . . . . . . . 15
⊢
(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ V |
| 76 | 73, 65, 75 | fvmpt 7016 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ → ((𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))‘𝑖) = (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 77 | 71, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))‘𝑖) = (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 78 | 77 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘((𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))‘𝑖)) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 79 | 70, 78 | eqtrd 2777 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))‘𝑖) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 80 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
| 81 | 80, 1 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
| 82 | | inss2 4238 |
. . . . . . . . . . . . 13
⊢
(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) |
| 83 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 84 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...𝑚) → 𝑗 ∈ ℕ) |
| 85 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 86 | 83, 84, 85 | syl2an 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 87 | 86 | elin2d 4205 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐺‘𝑗) ∈ (ℝ ×
ℝ)) |
| 88 | | 1st2nd2 8053 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) →
(𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
| 89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
| 90 | 89 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((,)‘(𝐺‘𝑗)) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉)) |
| 91 | | df-ov 7434 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉) |
| 92 | 90, 91 | eqtr4di 2795 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((,)‘(𝐺‘𝑗)) = ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗)))) |
| 93 | | ioossre 13448 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ⊆ ℝ |
| 94 | 92, 93 | eqsstrdi 4028 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
| 95 | 94 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
| 96 | 92 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((,)‘(𝐺‘𝑗))) = (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗))))) |
| 97 | | ovolfcl 25501 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐺‘𝑗)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑗)) ≤ (2nd
‘(𝐺‘𝑗)))) |
| 98 | 83, 84, 97 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
| 99 | | ovolioo 25603 |
. . . . . . . . . . . . . . . . 17
⊢
(((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗))) → (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗)))) = ((2nd
‘(𝐺‘𝑗)) − (1st
‘(𝐺‘𝑗)))) |
| 100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗)))) = ((2nd
‘(𝐺‘𝑗)) − (1st
‘(𝐺‘𝑗)))) |
| 101 | 96, 100 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((,)‘(𝐺‘𝑗))) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
| 102 | 98 | simp2d 1144 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
| 103 | 98 | simp1d 1143 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
| 104 | 102, 103 | resubcld 11691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
| 105 | 101, 104 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) |
| 106 | 105 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) |
| 107 | | ovolsscl 25521 |
. . . . . . . . . . . . 13
⊢
(((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) →
(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 108 | 82, 95, 106, 107 | mp3an2i 1468 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) |
| 109 | 108 | recnd 11289 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑚 ∈ ℕ ∧
(abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < )))
< 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℂ) |
| 110 | 79, 81, 109 | fsumser 15766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))))‘𝑛)) |
| 111 | 110 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → (seq1( + , (vol*
∘ (𝑧 ∈ ℕ
↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))))‘𝑛) = Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 112 | | 2fveq3 6911 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑘 → ((,)‘(𝐹‘𝑧)) = ((,)‘(𝐹‘𝑘))) |
| 113 | 112 | ineq1d 4219 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑘 → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐹‘𝑘)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 114 | 113 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) = (𝑘 ∈ ℕ ↦ (((,)‘(𝐹‘𝑘)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 115 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑧 = ∅ ↔ 𝑥 = ∅)) |
| 116 | | infeq1 9516 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → inf(𝑧, ℝ*, < ) = inf(𝑥, ℝ*, <
)) |
| 117 | | supeq1 9485 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → sup(𝑧, ℝ*, < ) = sup(𝑥, ℝ*, <
)) |
| 118 | 116, 117 | opeq12d 4881 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → 〈inf(𝑧, ℝ*, < ), sup(𝑧, ℝ*, <
)〉 = 〈inf(𝑥,
ℝ*, < ), sup(𝑥, ℝ*, <
)〉) |
| 119 | 115, 118 | ifbieq2d 4552 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → if(𝑧 = ∅, 〈0, 0〉, 〈inf(𝑧, ℝ*, < ),
sup(𝑧, ℝ*,
< )〉) = if(𝑥 =
∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, <
)〉)) |
| 120 | 119 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ran (,) ↦ if(𝑧 = ∅, 〈0, 0〉,
〈inf(𝑧,
ℝ*, < ), sup(𝑧, ℝ*, < )〉)) =
(𝑥 ∈ ran (,) ↦
if(𝑥 = ∅, 〈0,
0〉, 〈inf(𝑥,
ℝ*, < ), sup(𝑥, ℝ*, <
)〉)) |
| 121 | 16, 17, 18, 19, 20, 3, 7, 21, 5,
22, 114, 120 | uniioombllem2 25618 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → seq1( + , (vol*
∘ (𝑧 ∈ ℕ
↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))) ⇝ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴))) |
| 122 | 84, 121 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑚)) → seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))) ⇝ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴))) |
| 123 | 122 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))))) ⇝ (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴))) |
| 124 | 1, 57, 61, 111, 123 | climi2 15547 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ∃𝑎 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 125 | | 1z 12647 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
| 126 | 1 | rexuz3 15387 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → (∃𝑎
∈ ℕ ∀𝑛
∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))) |
| 127 | 125, 126 | ax-mp 5 |
. . . . . . . 8
⊢
(∃𝑎 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 128 | 124, 127 | sylib 218 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 129 | 128 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∀𝑗 ∈ (1...𝑚)∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 130 | | fzfi 14013 |
. . . . . . 7
⊢
(1...𝑚) ∈
Fin |
| 131 | | rexfiuz 15386 |
. . . . . . 7
⊢
((1...𝑚) ∈ Fin
→ (∃𝑎 ∈
ℤ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∀𝑗 ∈ (1...𝑚)∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))) |
| 132 | 130, 131 | ax-mp 5 |
. . . . . 6
⊢
(∃𝑎 ∈
ℤ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∀𝑗 ∈ (1...𝑚)∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 133 | 129, 132 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∃𝑎 ∈ ℤ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 134 | 1 | rexuz3 15387 |
. . . . . 6
⊢ (1 ∈
ℤ → (∃𝑎
∈ ℕ ∀𝑛
∈ (ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))) |
| 135 | 125, 134 | ax-mp 5 |
. . . . 5
⊢
(∃𝑎 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 136 | 133, 135 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∃𝑎 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 137 | 1 | r19.2uz 15390 |
. . . 4
⊢
(∃𝑎 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) → ∃𝑛 ∈ ℕ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 138 | 136, 137 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∃𝑛 ∈ ℕ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 139 | 16 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 140 | 17 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) |
| 141 | 20 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → (vol*‘𝐸) ∈ ℝ) |
| 142 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐶 ∈
ℝ+) |
| 143 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 144 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
| 145 | 22 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐸) + 𝐶)) |
| 146 | | simprll 779 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝑚 ∈ ℕ) |
| 147 | | simprlr 780 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) |
| 148 | | eqid 2737 |
. . . . 5
⊢ ∪ (((,) ∘ 𝐺) “ (1...𝑚)) = ∪ (((,)
∘ 𝐺) “
(1...𝑚)) |
| 149 | | simprrl 781 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝑛 ∈ ℕ) |
| 150 | | simprrr 782 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 151 | | 2fveq3 6911 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑧 → ((,)‘(𝐹‘𝑖)) = ((,)‘(𝐹‘𝑧))) |
| 152 | 151 | ineq1d 4219 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑧 → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 153 | 152 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑧 → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))))) |
| 154 | 153 | cbvsumv 15732 |
. . . . . . . . . . 11
⊢
Σ𝑖 ∈
(1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) |
| 155 | | 2fveq3 6911 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑘 → ((,)‘(𝐺‘𝑗)) = ((,)‘(𝐺‘𝑘))) |
| 156 | 155 | ineq2d 4220 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) |
| 157 | 156 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘))))) |
| 158 | 157 | sumeq2sdv 15739 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘))))) |
| 159 | 154, 158 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘))))) |
| 160 | 155 | ineq1d 4219 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (((,)‘(𝐺‘𝑗)) ∩ 𝐴) = (((,)‘(𝐺‘𝑘)) ∩ 𝐴)) |
| 161 | 160 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴))) |
| 162 | 159, 161 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴))) = (Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) − (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴)))) |
| 163 | 162 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) = (abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) − (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴))))) |
| 164 | 163 | breq1d 5153 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ (abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) − (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴)))) < (𝐶 / 𝑚))) |
| 165 | 164 | cbvralvw 3237 |
. . . . . 6
⊢
(∀𝑗 ∈
(1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∀𝑘 ∈ (1...𝑚)(abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) − (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 166 | 150, 165 | sylib 218 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → ∀𝑘 ∈ (1...𝑚)(abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝑘)))) − (vol*‘(((,)‘(𝐺‘𝑘)) ∩ 𝐴)))) < (𝐶 / 𝑚)) |
| 167 | | eqid 2737 |
. . . . 5
⊢ ∪ (((,) ∘ 𝐹) “ (1...𝑛)) = ∪ (((,)
∘ 𝐹) “
(1...𝑛)) |
| 168 | 139, 140,
18, 19, 141, 142, 143, 144, 5, 145, 146, 147, 148, 149, 166, 167 | uniioombllem5 25622 |
. . . 4
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) |
| 169 | 168 | anassrs 467 |
. . 3
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))) → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) |
| 170 | 138, 169 | rexlimddv 3161 |
. 2
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇‘𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) |
| 171 | 56, 170 | rexlimddv 3161 |
1
⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) |