| Step | Hyp | Ref
| Expression |
| 1 | | nnuz 12921 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
| 2 | | eqid 2737 |
. . 3
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))) = seq1( + , ((abs ∘ − )
∘ (𝐾 ∘ 𝐻))) |
| 3 | | 1zzd 12648 |
. . 3
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 1 ∈
ℤ) |
| 4 | | eqidd 2738 |
. . 3
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ (𝐾
∘ 𝐻))‘𝑛) = (((abs ∘ − )
∘ (𝐾 ∘ 𝐻))‘𝑛)) |
| 5 | | uniioombl.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 6 | | uniioombl.2 |
. . . . . . . . . 10
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
| 7 | | uniioombl.3 |
. . . . . . . . . 10
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
| 8 | | uniioombl.a |
. . . . . . . . . 10
⊢ 𝐴 = ∪
ran ((,) ∘ 𝐹) |
| 9 | | uniioombl.e |
. . . . . . . . . 10
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) |
| 10 | | uniioombl.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
| 11 | | uniioombl.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 12 | | uniioombl.s |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐺)) |
| 13 | | uniioombl.t |
. . . . . . . . . 10
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
| 14 | | uniioombl.v |
. . . . . . . . . 10
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐸) + 𝐶)) |
| 15 | 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | uniioombllem2a 25617 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ ran (,)) |
| 16 | | uniioombllem2.h |
. . . . . . . . . 10
⊢ 𝐻 = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) |
| 17 | 16 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 𝐻 = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))) |
| 18 | | uniioombllem2.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉)) |
| 19 | 18 | ioorf 25608 |
. . . . . . . . . . 11
⊢ 𝐾:ran (,)⟶( ≤ ∩
(ℝ* × ℝ*)) |
| 20 | 19 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 𝐾:ran (,)⟶( ≤ ∩
(ℝ* × ℝ*))) |
| 21 | 20 | feqmptd 6977 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 𝐾 = (𝑦 ∈ ran (,) ↦ (𝐾‘𝑦))) |
| 22 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) → (𝐾‘𝑦) = (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))) |
| 23 | 15, 17, 21, 22 | fmptco 7149 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐾 ∘ 𝐻) = (𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))))) |
| 24 | | inss2 4238 |
. . . . . . . . . . 11
⊢
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ⊆ ((,)‘(𝐺‘𝐽)) |
| 25 | | inss2 4238 |
. . . . . . . . . . . . . . . 16
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 26 | 11 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐺‘𝐽) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 27 | 25, 26 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐺‘𝐽) ∈ (ℝ ×
ℝ)) |
| 28 | | 1st2nd2 8053 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝐽) ∈ (ℝ × ℝ) →
(𝐺‘𝐽) = 〈(1st ‘(𝐺‘𝐽)), (2nd ‘(𝐺‘𝐽))〉) |
| 29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐺‘𝐽) = 〈(1st ‘(𝐺‘𝐽)), (2nd ‘(𝐺‘𝐽))〉) |
| 30 | 29 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((,)‘(𝐺‘𝐽)) = ((,)‘〈(1st
‘(𝐺‘𝐽)), (2nd
‘(𝐺‘𝐽))〉)) |
| 31 | | df-ov 7434 |
. . . . . . . . . . . . 13
⊢
((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽))) = ((,)‘〈(1st
‘(𝐺‘𝐽)), (2nd
‘(𝐺‘𝐽))〉) |
| 32 | 30, 31 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((,)‘(𝐺‘𝐽)) = ((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽)))) |
| 33 | | ioossre 13448 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽))) ⊆ ℝ |
| 34 | 32, 33 | eqsstrdi 4028 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((,)‘(𝐺‘𝐽)) ⊆ ℝ) |
| 35 | 32 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) →
(vol*‘((,)‘(𝐺‘𝐽))) = (vol*‘((1st
‘(𝐺‘𝐽))(,)(2nd
‘(𝐺‘𝐽))))) |
| 36 | | ovolfcl 25501 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐽 ∈ ℕ) → ((1st
‘(𝐺‘𝐽)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝐽)) ∈ ℝ ∧ (1st
‘(𝐺‘𝐽)) ≤ (2nd
‘(𝐺‘𝐽)))) |
| 37 | 11, 36 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((1st
‘(𝐺‘𝐽)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝐽)) ∈ ℝ ∧ (1st
‘(𝐺‘𝐽)) ≤ (2nd
‘(𝐺‘𝐽)))) |
| 38 | | ovolioo 25603 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(𝐺‘𝐽)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝐽)) ∈ ℝ ∧
(1st ‘(𝐺‘𝐽)) ≤ (2nd ‘(𝐺‘𝐽))) → (vol*‘((1st
‘(𝐺‘𝐽))(,)(2nd
‘(𝐺‘𝐽)))) = ((2nd
‘(𝐺‘𝐽)) − (1st
‘(𝐺‘𝐽)))) |
| 39 | 37, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) →
(vol*‘((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽)))) = ((2nd ‘(𝐺‘𝐽)) − (1st ‘(𝐺‘𝐽)))) |
| 40 | 35, 39 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) →
(vol*‘((,)‘(𝐺‘𝐽))) = ((2nd ‘(𝐺‘𝐽)) − (1st ‘(𝐺‘𝐽)))) |
| 41 | 37 | simp2d 1144 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (2nd
‘(𝐺‘𝐽)) ∈
ℝ) |
| 42 | 37 | simp1d 1143 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (1st
‘(𝐺‘𝐽)) ∈
ℝ) |
| 43 | 41, 42 | resubcld 11691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((2nd
‘(𝐺‘𝐽)) − (1st
‘(𝐺‘𝐽))) ∈
ℝ) |
| 44 | 40, 43 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) →
(vol*‘((,)‘(𝐺‘𝐽))) ∈ ℝ) |
| 45 | | ovolsscl 25521 |
. . . . . . . . . . 11
⊢
(((((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ⊆ ((,)‘(𝐺‘𝐽)) ∧ ((,)‘(𝐺‘𝐽)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝐽))) ∈ ℝ) →
(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) ∈ ℝ) |
| 46 | 24, 34, 44, 45 | mp3an2i 1468 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) →
(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) ∈ ℝ) |
| 47 | 46 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) →
(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) ∈ ℝ) |
| 48 | 18 | ioorcl 25612 |
. . . . . . . . 9
⊢
(((((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ ran (,) ∧
(vol*‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) ∈ ℝ) → (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 49 | 15, 47, 48 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 50 | 23, 49 | fmpt3d 7136 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐾 ∘ 𝐻):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 51 | | eqid 2737 |
. . . . . . . 8
⊢ ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)) = ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻)) |
| 52 | 51 | ovolfsf 25506 |
. . . . . . 7
⊢ ((𝐾 ∘ 𝐻):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻)):ℕ⟶(0[,)+∞)) |
| 53 | 50, 52 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((abs ∘
− ) ∘ (𝐾
∘ 𝐻)):ℕ⟶(0[,)+∞)) |
| 54 | 53 | ffvelcdmda 7104 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ (𝐾
∘ 𝐻))‘𝑛) ∈
(0[,)+∞)) |
| 55 | | elrege0 13494 |
. . . . 5
⊢ ((((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))‘𝑛) ∈ (0[,)+∞) ↔ ((((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ (𝐾
∘ 𝐻))‘𝑛))) |
| 56 | 54, 55 | sylib 218 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → ((((abs ∘
− ) ∘ (𝐾
∘ 𝐻))‘𝑛) ∈ ℝ ∧ 0 ≤
(((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))‘𝑛))) |
| 57 | 56 | simpld 494 |
. . 3
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ (𝐾
∘ 𝐻))‘𝑛) ∈
ℝ) |
| 58 | 56 | simprd 495 |
. . 3
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘
− ) ∘ (𝐾
∘ 𝐻))‘𝑛)) |
| 59 | 23 | fveq1d 6908 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((𝐾 ∘ 𝐻)‘𝑧) = ((𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))))‘𝑧)) |
| 60 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) ∈ V |
| 61 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))) = (𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))) |
| 62 | 61 | fvmpt2 7027 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℕ ∧ (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) ∈ V) → ((𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))))‘𝑧) = (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))) |
| 63 | 60, 62 | mpan2 691 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))))‘𝑧) = (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))) |
| 64 | 59, 63 | sylan9eq 2797 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((𝐾 ∘ 𝐻)‘𝑧) = (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))) |
| 65 | 64 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘((𝐾 ∘ 𝐻)‘𝑧)) = ((,)‘(𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))))) |
| 66 | 18 | ioorinv 25611 |
. . . . . . . . . . . . . 14
⊢
((((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ ran (,) → ((,)‘(𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) |
| 67 | 15, 66 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘(𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) |
| 68 | 65, 67 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘((𝐾 ∘ 𝐻)‘𝑧)) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) |
| 69 | 68 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∀𝑧 ∈ ℕ
((,)‘((𝐾 ∘
𝐻)‘𝑧)) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) |
| 70 | | 2fveq3 6911 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → ((,)‘((𝐾 ∘ 𝐻)‘𝑧)) = ((,)‘((𝐾 ∘ 𝐻)‘𝑥))) |
| 71 | | 2fveq3 6911 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → ((,)‘(𝐹‘𝑧)) = ((,)‘(𝐹‘𝑥))) |
| 72 | 71 | ineq1d 4219 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) = (((,)‘(𝐹‘𝑥)) ∩ ((,)‘(𝐺‘𝐽)))) |
| 73 | 70, 72 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → (((,)‘((𝐾 ∘ 𝐻)‘𝑧)) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ↔ ((,)‘((𝐾 ∘ 𝐻)‘𝑥)) = (((,)‘(𝐹‘𝑥)) ∩ ((,)‘(𝐺‘𝐽))))) |
| 74 | 73 | rspccva 3621 |
. . . . . . . . . . 11
⊢
((∀𝑧 ∈
ℕ ((,)‘((𝐾
∘ 𝐻)‘𝑧)) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∧ 𝑥 ∈ ℕ) → ((,)‘((𝐾 ∘ 𝐻)‘𝑥)) = (((,)‘(𝐹‘𝑥)) ∩ ((,)‘(𝐺‘𝐽)))) |
| 75 | 69, 74 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑥 ∈ ℕ) → ((,)‘((𝐾 ∘ 𝐻)‘𝑥)) = (((,)‘(𝐹‘𝑥)) ∩ ((,)‘(𝐺‘𝐽)))) |
| 76 | | inss1 4237 |
. . . . . . . . . 10
⊢
(((,)‘(𝐹‘𝑥)) ∩ ((,)‘(𝐺‘𝐽))) ⊆ ((,)‘(𝐹‘𝑥)) |
| 77 | 75, 76 | eqsstrdi 4028 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑥 ∈ ℕ) → ((,)‘((𝐾 ∘ 𝐻)‘𝑥)) ⊆ ((,)‘(𝐹‘𝑥))) |
| 78 | 77 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∀𝑥 ∈ ℕ
((,)‘((𝐾 ∘
𝐻)‘𝑥)) ⊆ ((,)‘(𝐹‘𝑥))) |
| 79 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
| 80 | | disjss2 5113 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℕ ((,)‘((𝐾
∘ 𝐻)‘𝑥)) ⊆ ((,)‘(𝐹‘𝑥)) → (Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)) → Disj 𝑥 ∈ ℕ ((,)‘((𝐾 ∘ 𝐻)‘𝑥)))) |
| 81 | 78, 79, 80 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → Disj 𝑥 ∈ ℕ
((,)‘((𝐾 ∘
𝐻)‘𝑥))) |
| 82 | 50, 81, 2 | uniioovol 25614 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (vol*‘∪ ran ((,) ∘ (𝐾 ∘ 𝐻))) = sup(ran seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻))),
ℝ*, < )) |
| 83 | 67 | mpteq2dva 5242 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝑧 ∈ ℕ ↦ ((,)‘(𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))))) = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))) |
| 84 | | rexpssxrxp 11306 |
. . . . . . . . . . . . . 14
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 85 | 25, 84 | sstri 3993 |
. . . . . . . . . . . . 13
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 86 | 85, 49 | sselid 3981 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) ∈ (ℝ* ×
ℝ*)) |
| 87 | | ioof 13487 |
. . . . . . . . . . . . . 14
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 88 | 87 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) →
(,):(ℝ* × ℝ*)⟶𝒫
ℝ) |
| 89 | 88 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (,) = (𝑦 ∈ (ℝ*
× ℝ*) ↦ ((,)‘𝑦))) |
| 90 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) → ((,)‘𝑦) = ((,)‘(𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))))) |
| 91 | 86, 23, 89, 90 | fmptco 7149 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((,) ∘ (𝐾 ∘ 𝐻)) = (𝑧 ∈ ℕ ↦ ((,)‘(𝐾‘(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))))) |
| 92 | 83, 91, 17 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((,) ∘ (𝐾 ∘ 𝐻)) = 𝐻) |
| 93 | 92 | rneqd 5949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ran ((,) ∘
(𝐾 ∘ 𝐻)) = ran 𝐻) |
| 94 | 93 | unieqd 4920 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∪ ran ((,) ∘ (𝐾 ∘ 𝐻)) = ∪ ran 𝐻) |
| 95 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
((,)‘(𝐹‘𝑧)) ∈ V |
| 96 | 95 | inex1 5317 |
. . . . . . . . . . . . 13
⊢
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ V |
| 97 | 16 | fvmpt2 7027 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℕ ∧
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ V) → (𝐻‘𝑧) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) |
| 98 | 96, 97 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ → (𝐻‘𝑧) = (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽)))) |
| 99 | | incom 4209 |
. . . . . . . . . . . 12
⊢
(((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) = (((,)‘(𝐺‘𝐽)) ∩ ((,)‘(𝐹‘𝑧))) |
| 100 | 98, 99 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → (𝐻‘𝑧) = (((,)‘(𝐺‘𝐽)) ∩ ((,)‘(𝐹‘𝑧)))) |
| 101 | 100 | iuneq2i 5013 |
. . . . . . . . . 10
⊢ ∪ 𝑧 ∈ ℕ (𝐻‘𝑧) = ∪ 𝑧 ∈ ℕ
(((,)‘(𝐺‘𝐽)) ∩ ((,)‘(𝐹‘𝑧))) |
| 102 | | iunin2 5071 |
. . . . . . . . . 10
⊢ ∪ 𝑧 ∈ ℕ (((,)‘(𝐺‘𝐽)) ∩ ((,)‘(𝐹‘𝑧))) = (((,)‘(𝐺‘𝐽)) ∩ ∪
𝑧 ∈ ℕ
((,)‘(𝐹‘𝑧))) |
| 103 | 101, 102 | eqtri 2765 |
. . . . . . . . 9
⊢ ∪ 𝑧 ∈ ℕ (𝐻‘𝑧) = (((,)‘(𝐺‘𝐽)) ∩ ∪
𝑧 ∈ ℕ
((,)‘(𝐹‘𝑧))) |
| 104 | 15, 16 | fmptd 7134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 𝐻:ℕ⟶ran (,)) |
| 105 | 104 | ffnd 6737 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 𝐻 Fn ℕ) |
| 106 | | fniunfv 7267 |
. . . . . . . . . 10
⊢ (𝐻 Fn ℕ → ∪ 𝑧 ∈ ℕ (𝐻‘𝑧) = ∪ ran 𝐻) |
| 107 | 105, 106 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∪ 𝑧 ∈ ℕ (𝐻‘𝑧) = ∪ ran 𝐻) |
| 108 | 103, 107 | eqtr3id 2791 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (((,)‘(𝐺‘𝐽)) ∩ ∪
𝑧 ∈ ℕ
((,)‘(𝐹‘𝑧))) = ∪ ran 𝐻) |
| 109 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 110 | | fvco3 7008 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑧 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑧) = ((,)‘(𝐹‘𝑧))) |
| 111 | 109, 110 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑧) = ((,)‘(𝐹‘𝑧))) |
| 112 | 111 | iuneq2dv 5016 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∪ 𝑧 ∈ ℕ (((,) ∘ 𝐹)‘𝑧) = ∪ 𝑧 ∈ ℕ
((,)‘(𝐹‘𝑧))) |
| 113 | | ffn 6736 |
. . . . . . . . . . . . . 14
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
| 114 | 87, 113 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (,) Fn
(ℝ* × ℝ*) |
| 115 | | fss 6752 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 116 | 109, 85, 115 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 117 | | fnfco 6773 |
. . . . . . . . . . . . 13
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹) Fn ℕ) |
| 118 | 114, 116,
117 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((,) ∘ 𝐹) Fn ℕ) |
| 119 | | fniunfv 7267 |
. . . . . . . . . . . 12
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑧 ∈ ℕ (((,) ∘ 𝐹)‘𝑧) = ∪ ran ((,)
∘ 𝐹)) |
| 120 | 118, 119 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∪ 𝑧 ∈ ℕ (((,) ∘ 𝐹)‘𝑧) = ∪ ran ((,)
∘ 𝐹)) |
| 121 | 120, 8 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∪ 𝑧 ∈ ℕ (((,) ∘ 𝐹)‘𝑧) = 𝐴) |
| 122 | 112, 121 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∪ 𝑧 ∈ ℕ ((,)‘(𝐹‘𝑧)) = 𝐴) |
| 123 | 122 | ineq2d 4220 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (((,)‘(𝐺‘𝐽)) ∩ ∪
𝑧 ∈ ℕ
((,)‘(𝐹‘𝑧))) = (((,)‘(𝐺‘𝐽)) ∩ 𝐴)) |
| 124 | 94, 108, 123 | 3eqtr2d 2783 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∪ ran ((,) ∘ (𝐾 ∘ 𝐻)) = (((,)‘(𝐺‘𝐽)) ∩ 𝐴)) |
| 125 | 124 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (vol*‘∪ ran ((,) ∘ (𝐾 ∘ 𝐻))) = (vol*‘(((,)‘(𝐺‘𝐽)) ∩ 𝐴))) |
| 126 | 82, 125 | eqtr3d 2779 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → sup(ran seq1( + ,
((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))), ℝ*, < ) =
(vol*‘(((,)‘(𝐺‘𝐽)) ∩ 𝐴))) |
| 127 | | inss1 4237 |
. . . . . 6
⊢
(((,)‘(𝐺‘𝐽)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝐽)) |
| 128 | | ovolsscl 25521 |
. . . . . 6
⊢
(((((,)‘(𝐺‘𝐽)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝐽)) ∧ ((,)‘(𝐺‘𝐽)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝐽))) ∈ ℝ) →
(vol*‘(((,)‘(𝐺‘𝐽)) ∩ 𝐴)) ∈ ℝ) |
| 129 | 127, 34, 44, 128 | mp3an2i 1468 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) →
(vol*‘(((,)‘(𝐺‘𝐽)) ∩ 𝐴)) ∈ ℝ) |
| 130 | 126, 129 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → sup(ran seq1( + ,
((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))), ℝ*, < ) ∈
ℝ) |
| 131 | 51, 2 | ovolsf 25507 |
. . . . . . . . 9
⊢ ((𝐾 ∘ 𝐻):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))):ℕ⟶(0[,)+∞)) |
| 132 | 50, 131 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))):ℕ⟶(0[,)+∞)) |
| 133 | 132 | frnd 6744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) ⊆ (0[,)+∞)) |
| 134 | | icossxr 13472 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ* |
| 135 | 133, 134 | sstrdi 3996 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) ⊆
ℝ*) |
| 136 | 132 | ffnd 6737 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) Fn ℕ) |
| 137 | | fnfvelrn 7100 |
. . . . . . 7
⊢ ((seq1( +
, ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))) Fn ℕ ∧ 𝑦 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))‘𝑦) ∈ ran seq1( + , ((abs ∘ −
) ∘ (𝐾 ∘ 𝐻)))) |
| 138 | 136, 137 | sylan 580 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑦 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))‘𝑦) ∈ ran seq1( + , ((abs ∘ −
) ∘ (𝐾 ∘ 𝐻)))) |
| 139 | | supxrub 13366 |
. . . . . 6
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))) ⊆ ℝ* ∧ (seq1(
+ , ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻)))‘𝑦) ∈ ran seq1( + , ((abs ∘ −
) ∘ (𝐾 ∘ 𝐻)))) → (seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻))),
ℝ*, < )) |
| 140 | 135, 138,
139 | syl2an2r 685 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑦 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻))),
ℝ*, < )) |
| 141 | 140 | ralrimiva 3146 |
. . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∀𝑦 ∈ ℕ (seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻))),
ℝ*, < )) |
| 142 | | brralrspcev 5203 |
. . . 4
⊢ ((sup(ran
seq1( + , ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))), ℝ*, < ) ∈
ℝ ∧ ∀𝑦
∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻))),
ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻)))‘𝑦) ≤ 𝑥) |
| 143 | 130, 141,
142 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))‘𝑦) ≤ 𝑥) |
| 144 | 1, 2, 3, 4, 57, 58, 143 | isumsup2 15882 |
. 2
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) ⇝ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻))), ℝ, <
)) |
| 145 | 51 | ovolfs2 25606 |
. . . . 5
⊢ ((𝐾 ∘ 𝐻):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻)) = ((vol* ∘ (,)) ∘ (𝐾 ∘ 𝐻))) |
| 146 | 50, 145 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((abs ∘
− ) ∘ (𝐾
∘ 𝐻)) = ((vol*
∘ (,)) ∘ (𝐾
∘ 𝐻))) |
| 147 | | coass 6285 |
. . . . 5
⊢ ((vol*
∘ (,)) ∘ (𝐾
∘ 𝐻)) = (vol* ∘
((,) ∘ (𝐾 ∘
𝐻))) |
| 148 | 92 | coeq2d 5873 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (vol* ∘ ((,)
∘ (𝐾 ∘ 𝐻))) = (vol* ∘ 𝐻)) |
| 149 | 147, 148 | eqtrid 2789 |
. . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((vol* ∘ (,))
∘ (𝐾 ∘ 𝐻)) = (vol* ∘ 𝐻)) |
| 150 | 146, 149 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((abs ∘
− ) ∘ (𝐾
∘ 𝐻)) = (vol* ∘
𝐻)) |
| 151 | 150 | seqeq3d 14050 |
. 2
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) = seq1( + , (vol* ∘ 𝐻))) |
| 152 | | rge0ssre 13496 |
. . . . 5
⊢
(0[,)+∞) ⊆ ℝ |
| 153 | 133, 152 | sstrdi 3996 |
. . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) ⊆ ℝ) |
| 154 | | 1nn 12277 |
. . . . . . 7
⊢ 1 ∈
ℕ |
| 155 | 132 | fdmd 6746 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → dom seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) = ℕ) |
| 156 | 154, 155 | eleqtrrid 2848 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 1 ∈ dom seq1( +
, ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻)))) |
| 157 | 156 | ne0d 4342 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → dom seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) ≠ ∅) |
| 158 | | dm0rn0 5935 |
. . . . . 6
⊢ (dom
seq1( + , ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))) = ∅ ↔ ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) = ∅) |
| 159 | 158 | necon3bii 2993 |
. . . . 5
⊢ (dom
seq1( + , ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))) ≠ ∅ ↔ ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) ≠ ∅) |
| 160 | 157, 159 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻))) ≠ ∅) |
| 161 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑧 = (seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻)))‘𝑦) → (𝑧 ≤ 𝑥 ↔ (seq1( + , ((abs ∘ − )
∘ (𝐾 ∘ 𝐻)))‘𝑦) ≤ 𝑥)) |
| 162 | 161 | ralrn 7108 |
. . . . . . 7
⊢ (seq1( +
, ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))) Fn ℕ → (∀𝑧 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))𝑧 ≤ 𝑥 ↔ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻)))‘𝑦) ≤ 𝑥)) |
| 163 | 136, 162 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (∀𝑧 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))𝑧 ≤ 𝑥 ↔ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻)))‘𝑦) ≤ 𝑥)) |
| 164 | 163 | rexbidv 3179 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻)))‘𝑦) ≤ 𝑥)) |
| 165 | 143, 164 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))𝑧 ≤ 𝑥) |
| 166 | | supxrre 13369 |
. . . 4
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))) ⊆ ℝ ∧ ran seq1( + ,
((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , ((abs
∘ − ) ∘ (𝐾 ∘ 𝐻)))𝑧 ≤ 𝑥) → sup(ran seq1( + , ((abs ∘
− ) ∘ (𝐾
∘ 𝐻))),
ℝ*, < ) = sup(ran seq1( + , ((abs ∘ − ) ∘
(𝐾 ∘ 𝐻))), ℝ, <
)) |
| 167 | 153, 160,
165, 166 | syl3anc 1373 |
. . 3
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → sup(ran seq1( + ,
((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))), ℝ*, < ) = sup(ran
seq1( + , ((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))), ℝ, < )) |
| 168 | 167, 126 | eqtr3d 2779 |
. 2
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → sup(ran seq1( + ,
((abs ∘ − ) ∘ (𝐾 ∘ 𝐻))), ℝ, < ) =
(vol*‘(((,)‘(𝐺‘𝐽)) ∩ 𝐴))) |
| 169 | 144, 151,
168 | 3brtr3d 5174 |
1
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → seq1( + , (vol*
∘ 𝐻)) ⇝
(vol*‘(((,)‘(𝐺‘𝐽)) ∩ 𝐴))) |