Step | Hyp | Ref
| Expression |
1 | | ovoliun.a |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) |
2 | 1 | ralrimiva 3107 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
3 | | iunss 4971 |
. . . 4
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀𝑛 ∈ ℕ 𝐴 ⊆
ℝ) |
4 | 2, 3 | sylibr 233 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
5 | | ovolcl 24547 |
. . 3
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
7 | | ovoliun.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)) |
8 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)) |
9 | | ovoliun.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) |
10 | | f1of 6700 |
. . . . . . . . . . . 12
⊢ (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → 𝐽:ℕ⟶(ℕ ×
ℕ)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽:ℕ⟶(ℕ ×
ℕ)) |
12 | 11 | ffvelrnda 6943 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐽‘𝑘) ∈ (ℕ ×
ℕ)) |
13 | | xp1st 7836 |
. . . . . . . . . 10
⊢ ((𝐽‘𝑘) ∈ (ℕ × ℕ) →
(1st ‘(𝐽‘𝑘)) ∈ ℕ) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐽‘𝑘)) ∈
ℕ) |
15 | 8, 14 | ffvelrnd 6944 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽‘𝑘))) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) |
16 | | elovolmlem 24543 |
. . . . . . . 8
⊢ ((𝐹‘(1st
‘(𝐽‘𝑘))) ∈ (( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ↔ (𝐹‘(1st
‘(𝐽‘𝑘))):ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
17 | 15, 16 | sylib 217 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽‘𝑘))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
18 | | xp2nd 7837 |
. . . . . . . 8
⊢ ((𝐽‘𝑘) ∈ (ℕ × ℕ) →
(2nd ‘(𝐽‘𝑘)) ∈ ℕ) |
19 | 12, 18 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐽‘𝑘)) ∈
ℕ) |
20 | 17, 19 | ffvelrnd 6944 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
21 | | ovoliun.h |
. . . . . 6
⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘)))) |
22 | 20, 21 | fmptd 6970 |
. . . . 5
⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
23 | | eqid 2738 |
. . . . . 6
⊢ ((abs
∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻) |
24 | | ovoliun.u |
. . . . . 6
⊢ 𝑈 = seq1( + , ((abs ∘
− ) ∘ 𝐻)) |
25 | 23, 24 | ovolsf 24541 |
. . . . 5
⊢ (𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞)) |
26 | | frn 6591 |
. . . . 5
⊢ (𝑈:ℕ⟶(0[,)+∞)
→ ran 𝑈 ⊆
(0[,)+∞)) |
27 | 22, 25, 26 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran 𝑈 ⊆ (0[,)+∞)) |
28 | | icossxr 13093 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ* |
29 | 27, 28 | sstrdi 3929 |
. . 3
⊢ (𝜑 → ran 𝑈 ⊆
ℝ*) |
30 | | supxrcl 12978 |
. . 3
⊢ (ran
𝑈 ⊆
ℝ* → sup(ran 𝑈, ℝ*, < ) ∈
ℝ*) |
31 | 29, 30 | syl 17 |
. 2
⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) ∈
ℝ*) |
32 | | ovoliun.r |
. . . 4
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
33 | | ovoliun.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
34 | 33 | rpred 12701 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
35 | 32, 34 | readdcld 10935 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) + 𝐵) ∈
ℝ) |
36 | 35 | rexrd 10956 |
. 2
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) + 𝐵) ∈
ℝ*) |
37 | | eliun 4925 |
. . . . . 6
⊢ (𝑧 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ↔ ∃𝑛 ∈ ℕ 𝑧 ∈ 𝐴) |
38 | | ovoliun.x1 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛))) |
39 | 38 | 3adant3 1130 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → 𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛))) |
40 | 1 | 3adant3 1130 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → 𝐴 ⊆ ℝ) |
41 | 7 | ffvelrnda 6943 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) |
42 | | elovolmlem 24543 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ↔ (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
43 | 41, 42 | sylib 217 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
44 | 43 | 3adant3 1130 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
45 | | ovolfioo 24536 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))))) |
46 | 40, 44, 45 | syl2anc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → (𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))))) |
47 | 39, 46 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → ∀𝑧 ∈ 𝐴 ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗)))) |
48 | | simp3 1136 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
49 | | rsp 3129 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝐴 ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))) → (𝑧 ∈ 𝐴 → ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))))) |
50 | 47, 48, 49 | sylc 65 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗)))) |
51 | | simpl1 1189 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → 𝜑) |
52 | | f1ocnv 6712 |
. . . . . . . . . . . 12
⊢ (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → ◡𝐽:(ℕ × ℕ)–1-1-onto→ℕ) |
53 | | f1of 6700 |
. . . . . . . . . . . 12
⊢ (◡𝐽:(ℕ × ℕ)–1-1-onto→ℕ → ◡𝐽:(ℕ ×
ℕ)⟶ℕ) |
54 | 51, 9, 52, 53 | 4syl 19 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → ◡𝐽:(ℕ ×
ℕ)⟶ℕ) |
55 | | simpl2 1190 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → 𝑛 ∈ ℕ) |
56 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
57 | 54, 55, 56 | fovrnd 7422 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝑛◡𝐽𝑗) ∈ ℕ) |
58 | | 2fveq3 6761 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = (𝑛◡𝐽𝑗) → (1st ‘(𝐽‘𝑘)) = (1st ‘(𝐽‘(𝑛◡𝐽𝑗)))) |
59 | 58 | fveq2d 6760 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑛◡𝐽𝑗) → (𝐹‘(1st ‘(𝐽‘𝑘))) = (𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗))))) |
60 | | 2fveq3 6761 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑛◡𝐽𝑗) → (2nd ‘(𝐽‘𝑘)) = (2nd ‘(𝐽‘(𝑛◡𝐽𝑗)))) |
61 | 59, 60 | fveq12d 6763 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑛◡𝐽𝑗) → ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))) = ((𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗))))‘(2nd ‘(𝐽‘(𝑛◡𝐽𝑗))))) |
62 | | fvex 6769 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘(1st
‘(𝐽‘(𝑛◡𝐽𝑗))))‘(2nd ‘(𝐽‘(𝑛◡𝐽𝑗)))) ∈ V |
63 | 61, 21, 62 | fvmpt 6857 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛◡𝐽𝑗) ∈ ℕ → (𝐻‘(𝑛◡𝐽𝑗)) = ((𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗))))‘(2nd ‘(𝐽‘(𝑛◡𝐽𝑗))))) |
64 | 57, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝐻‘(𝑛◡𝐽𝑗)) = ((𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗))))‘(2nd ‘(𝐽‘(𝑛◡𝐽𝑗))))) |
65 | | df-ov 7258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛◡𝐽𝑗) = (◡𝐽‘〈𝑛, 𝑗〉) |
66 | 65 | fveq2i 6759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐽‘(𝑛◡𝐽𝑗)) = (𝐽‘(◡𝐽‘〈𝑛, 𝑗〉)) |
67 | 51, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) |
68 | 55, 56 | opelxpd 5618 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → 〈𝑛, 𝑗〉 ∈ (ℕ ×
ℕ)) |
69 | | f1ocnvfv2 7130 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐽:ℕ–1-1-onto→(ℕ × ℕ) ∧ 〈𝑛, 𝑗〉 ∈ (ℕ × ℕ))
→ (𝐽‘(◡𝐽‘〈𝑛, 𝑗〉)) = 〈𝑛, 𝑗〉) |
70 | 67, 68, 69 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝐽‘(◡𝐽‘〈𝑛, 𝑗〉)) = 〈𝑛, 𝑗〉) |
71 | 66, 70 | syl5eq 2791 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝐽‘(𝑛◡𝐽𝑗)) = 〈𝑛, 𝑗〉) |
72 | 71 | fveq2d 6760 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (1st
‘(𝐽‘(𝑛◡𝐽𝑗))) = (1st ‘〈𝑛, 𝑗〉)) |
73 | | vex 3426 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑛 ∈ V |
74 | | vex 3426 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑗 ∈ V |
75 | 73, 74 | op1st 7812 |
. . . . . . . . . . . . . . . . . 18
⊢
(1st ‘〈𝑛, 𝑗〉) = 𝑛 |
76 | 72, 75 | eqtrdi 2795 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (1st
‘(𝐽‘(𝑛◡𝐽𝑗))) = 𝑛) |
77 | 76 | fveq2d 6760 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗)))) = (𝐹‘𝑛)) |
78 | 71 | fveq2d 6760 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (2nd
‘(𝐽‘(𝑛◡𝐽𝑗))) = (2nd ‘〈𝑛, 𝑗〉)) |
79 | 73, 74 | op2nd 7813 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘〈𝑛, 𝑗〉) = 𝑗 |
80 | 78, 79 | eqtrdi 2795 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (2nd
‘(𝐽‘(𝑛◡𝐽𝑗))) = 𝑗) |
81 | 77, 80 | fveq12d 6763 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗))))‘(2nd ‘(𝐽‘(𝑛◡𝐽𝑗)))) = ((𝐹‘𝑛)‘𝑗)) |
82 | 64, 81 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝐻‘(𝑛◡𝐽𝑗)) = ((𝐹‘𝑛)‘𝑗)) |
83 | 82 | fveq2d 6760 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (1st
‘(𝐻‘(𝑛◡𝐽𝑗))) = (1st ‘((𝐹‘𝑛)‘𝑗))) |
84 | 83 | breq1d 5080 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧 ↔ (1st ‘((𝐹‘𝑛)‘𝑗)) < 𝑧)) |
85 | 82 | fveq2d 6760 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (2nd
‘(𝐻‘(𝑛◡𝐽𝑗))) = (2nd ‘((𝐹‘𝑛)‘𝑗))) |
86 | 85 | breq2d 5082 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗))) ↔ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗)))) |
87 | 84, 86 | anbi12d 630 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (((1st
‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗)))) ↔ ((1st ‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))))) |
88 | 87 | biimprd 247 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))) → ((1st ‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗)))))) |
89 | | 2fveq3 6761 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛◡𝐽𝑗) → (1st ‘(𝐻‘𝑚)) = (1st ‘(𝐻‘(𝑛◡𝐽𝑗)))) |
90 | 89 | breq1d 5080 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛◡𝐽𝑗) → ((1st ‘(𝐻‘𝑚)) < 𝑧 ↔ (1st ‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧)) |
91 | | 2fveq3 6761 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛◡𝐽𝑗) → (2nd ‘(𝐻‘𝑚)) = (2nd ‘(𝐻‘(𝑛◡𝐽𝑗)))) |
92 | 91 | breq2d 5082 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛◡𝐽𝑗) → (𝑧 < (2nd ‘(𝐻‘𝑚)) ↔ 𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗))))) |
93 | 90, 92 | anbi12d 630 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛◡𝐽𝑗) → (((1st ‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))) ↔ ((1st ‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗)))))) |
94 | 93 | rspcev 3552 |
. . . . . . . . . 10
⊢ (((𝑛◡𝐽𝑗) ∈ ℕ ∧ ((1st
‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗))))) → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚)))) |
95 | 57, 88, 94 | syl6an 680 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))) → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
96 | 95 | rexlimdva 3212 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → (∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))) → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
97 | 50, 96 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚)))) |
98 | 97 | rexlimdv3a 3214 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ ℕ 𝑧 ∈ 𝐴 → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
99 | 37, 98 | syl5bi 241 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ∪
𝑛 ∈ ℕ 𝐴 → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
100 | 99 | ralrimiv 3106 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ∪
𝑛 ∈ ℕ 𝐴∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚)))) |
101 | | ovolfioo 24536 |
. . . . 5
⊢
((∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) → (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐻) ↔ ∀𝑧 ∈ ∪
𝑛 ∈ ℕ 𝐴∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
102 | 4, 22, 101 | syl2anc 583 |
. . . 4
⊢ (𝜑 → (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran
((,) ∘ 𝐻) ↔
∀𝑧 ∈ ∪ 𝑛 ∈ ℕ 𝐴∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
103 | 100, 102 | mpbird 256 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran
((,) ∘ 𝐻)) |
104 | 24 | ovollb 24548 |
. . 3
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐻)) → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑈, ℝ*, <
)) |
105 | 22, 103, 104 | syl2anc 583 |
. 2
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑈, ℝ*, <
)) |
106 | | fzfi 13620 |
. . . . . . 7
⊢
(1...𝑗) ∈
Fin |
107 | | elfznn 13214 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (1...𝑗) → 𝑤 ∈ ℕ) |
108 | | ffvelrn 6941 |
. . . . . . . . . . 11
⊢ ((𝐽:ℕ⟶(ℕ ×
ℕ) ∧ 𝑤 ∈
ℕ) → (𝐽‘𝑤) ∈ (ℕ ×
ℕ)) |
109 | | xp1st 7836 |
. . . . . . . . . . 11
⊢ ((𝐽‘𝑤) ∈ (ℕ × ℕ) →
(1st ‘(𝐽‘𝑤)) ∈ ℕ) |
110 | | nnre 11910 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐽‘𝑤)) ∈ ℕ → (1st
‘(𝐽‘𝑤)) ∈
ℝ) |
111 | 108, 109,
110 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝐽:ℕ⟶(ℕ ×
ℕ) ∧ 𝑤 ∈
ℕ) → (1st ‘(𝐽‘𝑤)) ∈ ℝ) |
112 | 11, 107, 111 | syl2an 595 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑗)) → (1st ‘(𝐽‘𝑤)) ∈ ℝ) |
113 | 112 | ralrimiva 3107 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ∈ ℝ) |
114 | 113 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ∈ ℝ) |
115 | | fimaxre3 11851 |
. . . . . . 7
⊢
(((1...𝑗) ∈ Fin
∧ ∀𝑤 ∈
(1...𝑗)(1st
‘(𝐽‘𝑤)) ∈ ℝ) →
∃𝑥 ∈ ℝ
∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥) |
116 | 106, 114,
115 | sylancr 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥) |
117 | | fllep1 13449 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
118 | 117 | ad2antlr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
119 | 112 | adantlr 711 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → (1st ‘(𝐽‘𝑤)) ∈ ℝ) |
120 | | simplr 765 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → 𝑥 ∈ ℝ) |
121 | | flcl 13443 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℤ) |
122 | 121 | peano2zd 12358 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ →
((⌊‘𝑥) + 1)
∈ ℤ) |
123 | 122 | zred 12355 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
((⌊‘𝑥) + 1)
∈ ℝ) |
124 | 123 | ad2antlr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → ((⌊‘𝑥) + 1) ∈ ℝ) |
125 | | letr 10999 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐽‘𝑤)) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ((⌊‘𝑥) + 1) ∈ ℝ) →
(((1st ‘(𝐽‘𝑤)) ≤ 𝑥 ∧ 𝑥 ≤ ((⌊‘𝑥) + 1)) → (1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) |
126 | 119, 120,
124, 125 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → (((1st ‘(𝐽‘𝑤)) ≤ 𝑥 ∧ 𝑥 ≤ ((⌊‘𝑥) + 1)) → (1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) |
127 | 118, 126 | mpan2d 690 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → ((1st ‘(𝐽‘𝑤)) ≤ 𝑥 → (1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) |
128 | 127 | ralimdva 3102 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥 → ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) |
129 | 128 | adantlr 711 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥 → ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) |
130 | | ovoliun.t |
. . . . . . . . . 10
⊢ 𝑇 = seq1( + , 𝐺) |
131 | | ovoliun.g |
. . . . . . . . . 10
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) |
132 | | simpll 763 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → 𝜑) |
133 | 132, 1 | sylan 579 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) |
134 | | ovoliun.v |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
135 | 132, 134 | sylan 579 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
136 | 132, 32 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
137 | 132, 33 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → 𝐵 ∈
ℝ+) |
138 | | ovoliun.s |
. . . . . . . . . 10
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ (𝐹‘𝑛))) |
139 | 132, 9 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) |
140 | 132, 7 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)) |
141 | 132, 38 | sylan 579 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛))) |
142 | | ovoliun.x2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
≤ ((vol*‘𝐴) +
(𝐵 / (2↑𝑛)))) |
143 | 132, 142 | sylan 579 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
≤ ((vol*‘𝐴) +
(𝐵 / (2↑𝑛)))) |
144 | | simplr 765 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → 𝑗 ∈ ℕ) |
145 | 122 | ad2antrl 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → ((⌊‘𝑥) + 1) ∈
ℤ) |
146 | | simprr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1)) |
147 | 130, 131,
133, 135, 136, 137, 138, 24, 21, 139, 140, 141, 143, 144, 145, 146 | ovoliunlem1 24571 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
148 | 147 | expr 456 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1) → (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
149 | 129, 148 | syld 47 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥 → (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
150 | 149 | rexlimdva 3212 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∃𝑥 ∈ ℝ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥 → (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
151 | 116, 150 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
152 | 151 | ralrimiva 3107 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
153 | | ffn 6584 |
. . . . 5
⊢ (𝑈:ℕ⟶(0[,)+∞)
→ 𝑈 Fn
ℕ) |
154 | | breq1 5073 |
. . . . . 6
⊢ (𝑧 = (𝑈‘𝑗) → (𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵) ↔ (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
155 | 154 | ralrn 6946 |
. . . . 5
⊢ (𝑈 Fn ℕ →
(∀𝑧 ∈ ran 𝑈 𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵) ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
156 | 22, 25, 153, 155 | 4syl 19 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵) ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
157 | 152, 156 | mpbird 256 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
158 | | supxrleub 12989 |
. . . 4
⊢ ((ran
𝑈 ⊆
ℝ* ∧ (sup(ran 𝑇, ℝ*, < ) + 𝐵) ∈ ℝ*)
→ (sup(ran 𝑈,
ℝ*, < ) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵) ↔ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
159 | 29, 36, 158 | syl2anc 583 |
. . 3
⊢ (𝜑 → (sup(ran 𝑈, ℝ*, < ) ≤ (sup(ran
𝑇, ℝ*,
< ) + 𝐵) ↔
∀𝑧 ∈ ran 𝑈 𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
160 | 157, 159 | mpbird 256 |
. 2
⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) ≤ (sup(ran
𝑇, ℝ*,
< ) + 𝐵)) |
161 | 6, 31, 36, 105, 160 | xrletrd 12825 |
1
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |