Step | Hyp | Ref
| Expression |
1 | | ovoliun.a |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) |
2 | 1 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
3 | | iunss 4497 |
. . . 4
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀𝑛 ∈ ℕ 𝐴 ⊆
ℝ) |
4 | 2, 3 | sylibr 223 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
5 | | ovolcl 23053 |
. . 3
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
7 | | ovoliun.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)) |
8 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)) |
9 | | ovoliun.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) |
10 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → 𝐽:ℕ⟶(ℕ ×
ℕ)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽:ℕ⟶(ℕ ×
ℕ)) |
12 | 11 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐽‘𝑘) ∈ (ℕ ×
ℕ)) |
13 | | xp1st 7089 |
. . . . . . . . . 10
⊢ ((𝐽‘𝑘) ∈ (ℕ × ℕ) →
(1st ‘(𝐽‘𝑘)) ∈ ℕ) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐽‘𝑘)) ∈
ℕ) |
15 | 8, 14 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽‘𝑘))) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
16 | | reex 9906 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
17 | 16, 16 | xpex 6860 |
. . . . . . . . . 10
⊢ (ℝ
× ℝ) ∈ V |
18 | 17 | inex2 4728 |
. . . . . . . . 9
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
19 | | nnex 10903 |
. . . . . . . . 9
⊢ ℕ
∈ V |
20 | 18, 19 | elmap 7772 |
. . . . . . . 8
⊢ ((𝐹‘(1st
‘(𝐽‘𝑘))) ∈ (( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ↔ (𝐹‘(1st
‘(𝐽‘𝑘))):ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
21 | 15, 20 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽‘𝑘))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
22 | | xp2nd 7090 |
. . . . . . . 8
⊢ ((𝐽‘𝑘) ∈ (ℕ × ℕ) →
(2nd ‘(𝐽‘𝑘)) ∈ ℕ) |
23 | 12, 22 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐽‘𝑘)) ∈
ℕ) |
24 | 21, 23 | ffvelrnd 6268 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
25 | | ovoliun.h |
. . . . . 6
⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘)))) |
26 | 24, 25 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
27 | | eqid 2610 |
. . . . . 6
⊢ ((abs
∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻) |
28 | | ovoliun.u |
. . . . . 6
⊢ 𝑈 = seq1( + , ((abs ∘
− ) ∘ 𝐻)) |
29 | 27, 28 | ovolsf 23048 |
. . . . 5
⊢ (𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞)) |
30 | | frn 5966 |
. . . . 5
⊢ (𝑈:ℕ⟶(0[,)+∞)
→ ran 𝑈 ⊆
(0[,)+∞)) |
31 | 26, 29, 30 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran 𝑈 ⊆ (0[,)+∞)) |
32 | | icossxr 12129 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ* |
33 | 31, 32 | syl6ss 3580 |
. . 3
⊢ (𝜑 → ran 𝑈 ⊆
ℝ*) |
34 | | supxrcl 12017 |
. . 3
⊢ (ran
𝑈 ⊆
ℝ* → sup(ran 𝑈, ℝ*, < ) ∈
ℝ*) |
35 | 33, 34 | syl 17 |
. 2
⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) ∈
ℝ*) |
36 | | ovoliun.r |
. . . 4
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
37 | | ovoliun.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
38 | 37 | rpred 11748 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
39 | 36, 38 | readdcld 9948 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) + 𝐵) ∈
ℝ) |
40 | 39 | rexrd 9968 |
. 2
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) + 𝐵) ∈
ℝ*) |
41 | | eliun 4460 |
. . . . . 6
⊢ (𝑧 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ↔ ∃𝑛 ∈ ℕ 𝑧 ∈ 𝐴) |
42 | | ovoliun.x1 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛))) |
43 | 42 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → 𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛))) |
44 | 1 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → 𝐴 ⊆ ℝ) |
45 | 7 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
46 | 18, 19 | elmap 7772 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ↔ (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
47 | 45, 46 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
48 | 47 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
49 | | ovolfioo 23043 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))))) |
50 | 44, 48, 49 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → (𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))))) |
51 | 43, 50 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → ∀𝑧 ∈ 𝐴 ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗)))) |
52 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
53 | | rsp 2913 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝐴 ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))) → (𝑧 ∈ 𝐴 → ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))))) |
54 | 51, 52, 53 | sylc 63 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → ∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗)))) |
55 | | simpl1 1057 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → 𝜑) |
56 | | f1ocnv 6062 |
. . . . . . . . . . . 12
⊢ (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → ◡𝐽:(ℕ × ℕ)–1-1-onto→ℕ) |
57 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (◡𝐽:(ℕ × ℕ)–1-1-onto→ℕ → ◡𝐽:(ℕ ×
ℕ)⟶ℕ) |
58 | 55, 9, 56, 57 | 4syl 19 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → ◡𝐽:(ℕ ×
ℕ)⟶ℕ) |
59 | | simpl2 1058 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → 𝑛 ∈ ℕ) |
60 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
61 | 58, 59, 60 | fovrnd 6704 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝑛◡𝐽𝑗) ∈ ℕ) |
62 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = (𝑛◡𝐽𝑗) → (𝐽‘𝑘) = (𝐽‘(𝑛◡𝐽𝑗))) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = (𝑛◡𝐽𝑗) → (1st ‘(𝐽‘𝑘)) = (1st ‘(𝐽‘(𝑛◡𝐽𝑗)))) |
64 | 63 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑛◡𝐽𝑗) → (𝐹‘(1st ‘(𝐽‘𝑘))) = (𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗))))) |
65 | 62 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑛◡𝐽𝑗) → (2nd ‘(𝐽‘𝑘)) = (2nd ‘(𝐽‘(𝑛◡𝐽𝑗)))) |
66 | 64, 65 | fveq12d 6109 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑛◡𝐽𝑗) → ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))) = ((𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗))))‘(2nd ‘(𝐽‘(𝑛◡𝐽𝑗))))) |
67 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘(1st
‘(𝐽‘(𝑛◡𝐽𝑗))))‘(2nd ‘(𝐽‘(𝑛◡𝐽𝑗)))) ∈ V |
68 | 66, 25, 67 | fvmpt 6191 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛◡𝐽𝑗) ∈ ℕ → (𝐻‘(𝑛◡𝐽𝑗)) = ((𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗))))‘(2nd ‘(𝐽‘(𝑛◡𝐽𝑗))))) |
69 | 61, 68 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝐻‘(𝑛◡𝐽𝑗)) = ((𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗))))‘(2nd ‘(𝐽‘(𝑛◡𝐽𝑗))))) |
70 | | df-ov 6552 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛◡𝐽𝑗) = (◡𝐽‘〈𝑛, 𝑗〉) |
71 | 70 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐽‘(𝑛◡𝐽𝑗)) = (𝐽‘(◡𝐽‘〈𝑛, 𝑗〉)) |
72 | 55, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) |
73 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) →
〈𝑛, 𝑗〉 ∈ (ℕ ×
ℕ)) |
74 | 59, 60, 73 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → 〈𝑛, 𝑗〉 ∈ (ℕ ×
ℕ)) |
75 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐽:ℕ–1-1-onto→(ℕ × ℕ) ∧ 〈𝑛, 𝑗〉 ∈ (ℕ × ℕ))
→ (𝐽‘(◡𝐽‘〈𝑛, 𝑗〉)) = 〈𝑛, 𝑗〉) |
76 | 72, 74, 75 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝐽‘(◡𝐽‘〈𝑛, 𝑗〉)) = 〈𝑛, 𝑗〉) |
77 | 71, 76 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝐽‘(𝑛◡𝐽𝑗)) = 〈𝑛, 𝑗〉) |
78 | 77 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (1st
‘(𝐽‘(𝑛◡𝐽𝑗))) = (1st ‘〈𝑛, 𝑗〉)) |
79 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑛 ∈ V |
80 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑗 ∈ V |
81 | 79, 80 | op1st 7067 |
. . . . . . . . . . . . . . . . . 18
⊢
(1st ‘〈𝑛, 𝑗〉) = 𝑛 |
82 | 78, 81 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (1st
‘(𝐽‘(𝑛◡𝐽𝑗))) = 𝑛) |
83 | 82 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗)))) = (𝐹‘𝑛)) |
84 | 77 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (2nd
‘(𝐽‘(𝑛◡𝐽𝑗))) = (2nd ‘〈𝑛, 𝑗〉)) |
85 | 79, 80 | op2nd 7068 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘〈𝑛, 𝑗〉) = 𝑗 |
86 | 84, 85 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (2nd
‘(𝐽‘(𝑛◡𝐽𝑗))) = 𝑗) |
87 | 83, 86 | fveq12d 6109 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(1st ‘(𝐽‘(𝑛◡𝐽𝑗))))‘(2nd ‘(𝐽‘(𝑛◡𝐽𝑗)))) = ((𝐹‘𝑛)‘𝑗)) |
88 | 69, 87 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝐻‘(𝑛◡𝐽𝑗)) = ((𝐹‘𝑛)‘𝑗)) |
89 | 88 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (1st
‘(𝐻‘(𝑛◡𝐽𝑗))) = (1st ‘((𝐹‘𝑛)‘𝑗))) |
90 | 89 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧 ↔ (1st ‘((𝐹‘𝑛)‘𝑗)) < 𝑧)) |
91 | 88 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (2nd
‘(𝐻‘(𝑛◡𝐽𝑗))) = (2nd ‘((𝐹‘𝑛)‘𝑗))) |
92 | 91 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗))) ↔ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗)))) |
93 | 90, 92 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (((1st
‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗)))) ↔ ((1st ‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))))) |
94 | 93 | biimprd 237 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))) → ((1st ‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗)))))) |
95 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛◡𝐽𝑗) → (𝐻‘𝑚) = (𝐻‘(𝑛◡𝐽𝑗))) |
96 | 95 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛◡𝐽𝑗) → (1st ‘(𝐻‘𝑚)) = (1st ‘(𝐻‘(𝑛◡𝐽𝑗)))) |
97 | 96 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛◡𝐽𝑗) → ((1st ‘(𝐻‘𝑚)) < 𝑧 ↔ (1st ‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧)) |
98 | 95 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛◡𝐽𝑗) → (2nd ‘(𝐻‘𝑚)) = (2nd ‘(𝐻‘(𝑛◡𝐽𝑗)))) |
99 | 98 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛◡𝐽𝑗) → (𝑧 < (2nd ‘(𝐻‘𝑚)) ↔ 𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗))))) |
100 | 97, 99 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛◡𝐽𝑗) → (((1st ‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))) ↔ ((1st ‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗)))))) |
101 | 100 | rspcev 3282 |
. . . . . . . . . 10
⊢ (((𝑛◡𝐽𝑗) ∈ ℕ ∧ ((1st
‘(𝐻‘(𝑛◡𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘(𝑛◡𝐽𝑗))))) → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚)))) |
102 | 61, 94, 101 | syl6an 566 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ ℕ) → (((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))) → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
103 | 102 | rexlimdva 3013 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → (∃𝑗 ∈ ℕ ((1st
‘((𝐹‘𝑛)‘𝑗)) < 𝑧 ∧ 𝑧 < (2nd ‘((𝐹‘𝑛)‘𝑗))) → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
104 | 54, 103 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴) → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚)))) |
105 | 104 | rexlimdv3a 3015 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ ℕ 𝑧 ∈ 𝐴 → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
106 | 41, 105 | syl5bi 231 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ∪
𝑛 ∈ ℕ 𝐴 → ∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
107 | 106 | ralrimiv 2948 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ∪
𝑛 ∈ ℕ 𝐴∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚)))) |
108 | | ovolfioo 23043 |
. . . . 5
⊢
((∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) → (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐻) ↔ ∀𝑧 ∈ ∪
𝑛 ∈ ℕ 𝐴∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
109 | 4, 26, 108 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran
((,) ∘ 𝐻) ↔
∀𝑧 ∈ ∪ 𝑛 ∈ ℕ 𝐴∃𝑚 ∈ ℕ ((1st
‘(𝐻‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐻‘𝑚))))) |
110 | 107, 109 | mpbird 246 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran
((,) ∘ 𝐻)) |
111 | 28 | ovollb 23054 |
. . 3
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐻)) → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑈, ℝ*, <
)) |
112 | 26, 110, 111 | syl2anc 691 |
. 2
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑈, ℝ*, <
)) |
113 | | fzfi 12633 |
. . . . . . 7
⊢
(1...𝑗) ∈
Fin |
114 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (1...𝑗) → 𝑤 ∈ ℕ) |
115 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐽:ℕ⟶(ℕ ×
ℕ) ∧ 𝑤 ∈
ℕ) → (𝐽‘𝑤) ∈ (ℕ ×
ℕ)) |
116 | | xp1st 7089 |
. . . . . . . . . . 11
⊢ ((𝐽‘𝑤) ∈ (ℕ × ℕ) →
(1st ‘(𝐽‘𝑤)) ∈ ℕ) |
117 | | nnre 10904 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐽‘𝑤)) ∈ ℕ → (1st
‘(𝐽‘𝑤)) ∈
ℝ) |
118 | 115, 116,
117 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝐽:ℕ⟶(ℕ ×
ℕ) ∧ 𝑤 ∈
ℕ) → (1st ‘(𝐽‘𝑤)) ∈ ℝ) |
119 | 11, 114, 118 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑗)) → (1st ‘(𝐽‘𝑤)) ∈ ℝ) |
120 | 119 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ∈ ℝ) |
121 | 120 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ∈ ℝ) |
122 | | fimaxre3 10849 |
. . . . . . 7
⊢
(((1...𝑗) ∈ Fin
∧ ∀𝑤 ∈
(1...𝑗)(1st
‘(𝐽‘𝑤)) ∈ ℝ) →
∃𝑥 ∈ ℝ
∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥) |
123 | 113, 121,
122 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥) |
124 | | fllep1 12464 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
125 | 124 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
126 | 119 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → (1st ‘(𝐽‘𝑤)) ∈ ℝ) |
127 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → 𝑥 ∈ ℝ) |
128 | | flcl 12458 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℤ) |
129 | 128 | peano2zd 11361 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ →
((⌊‘𝑥) + 1)
∈ ℤ) |
130 | 129 | zred 11358 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
((⌊‘𝑥) + 1)
∈ ℝ) |
131 | 130 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → ((⌊‘𝑥) + 1) ∈ ℝ) |
132 | | letr 10010 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐽‘𝑤)) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ((⌊‘𝑥) + 1) ∈ ℝ) →
(((1st ‘(𝐽‘𝑤)) ≤ 𝑥 ∧ 𝑥 ≤ ((⌊‘𝑥) + 1)) → (1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) |
133 | 126, 127,
131, 132 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → (((1st ‘(𝐽‘𝑤)) ≤ 𝑥 ∧ 𝑥 ≤ ((⌊‘𝑥) + 1)) → (1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) |
134 | 125, 133 | mpan2d 706 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ (1...𝑗)) → ((1st ‘(𝐽‘𝑤)) ≤ 𝑥 → (1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) |
135 | 134 | ralimdva 2945 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥 → ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) |
136 | 135 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥 → ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) |
137 | | ovoliun.t |
. . . . . . . . . 10
⊢ 𝑇 = seq1( + , 𝐺) |
138 | | ovoliun.g |
. . . . . . . . . 10
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) |
139 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → 𝜑) |
140 | 139, 1 | sylan 487 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) |
141 | | ovoliun.v |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
142 | 139, 141 | sylan 487 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
143 | 139, 36 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
144 | 139, 37 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → 𝐵 ∈
ℝ+) |
145 | | ovoliun.s |
. . . . . . . . . 10
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ (𝐹‘𝑛))) |
146 | 139, 9 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) |
147 | 139, 7 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)) |
148 | 139, 42 | sylan 487 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛))) |
149 | | ovoliun.x2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
≤ ((vol*‘𝐴) +
(𝐵 / (2↑𝑛)))) |
150 | 139, 149 | sylan 487 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
≤ ((vol*‘𝐴) +
(𝐵 / (2↑𝑛)))) |
151 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → 𝑗 ∈ ℕ) |
152 | 129 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → ((⌊‘𝑥) + 1) ∈
ℤ) |
153 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1)) |
154 | 137, 138,
140, 142, 143, 144, 145, 28, 25, 146, 147, 148, 150, 151, 152, 153 | ovoliunlem1 23077 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1))) → (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
155 | 154 | expr 641 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ ((⌊‘𝑥) + 1) → (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
156 | 136, 155 | syld 46 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥 → (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
157 | 156 | rexlimdva 3013 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∃𝑥 ∈ ℝ ∀𝑤 ∈ (1...𝑗)(1st ‘(𝐽‘𝑤)) ≤ 𝑥 → (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
158 | 123, 157 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
159 | 158 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
160 | | ffn 5958 |
. . . . 5
⊢ (𝑈:ℕ⟶(0[,)+∞)
→ 𝑈 Fn
ℕ) |
161 | | breq1 4586 |
. . . . . 6
⊢ (𝑧 = (𝑈‘𝑗) → (𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵) ↔ (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
162 | 161 | ralrn 6270 |
. . . . 5
⊢ (𝑈 Fn ℕ →
(∀𝑧 ∈ ran 𝑈 𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵) ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
163 | 26, 29, 160, 162 | 4syl 19 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵) ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
164 | 159, 163 | mpbird 246 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
165 | | supxrleub 12028 |
. . . 4
⊢ ((ran
𝑈 ⊆
ℝ* ∧ (sup(ran 𝑇, ℝ*, < ) + 𝐵) ∈ ℝ*)
→ (sup(ran 𝑈,
ℝ*, < ) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵) ↔ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
166 | 33, 40, 165 | syl2anc 691 |
. . 3
⊢ (𝜑 → (sup(ran 𝑈, ℝ*, < ) ≤ (sup(ran
𝑇, ℝ*,
< ) + 𝐵) ↔
∀𝑧 ∈ ran 𝑈 𝑧 ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
167 | 164, 166 | mpbird 246 |
. 2
⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) ≤ (sup(ran
𝑇, ℝ*,
< ) + 𝐵)) |
168 | 6, 35, 40, 112, 167 | xrletrd 11869 |
1
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |