Step | Hyp | Ref
| Expression |
1 | | nfcv 2907 |
. . . 4
⊢
Ⅎ𝑚𝐴 |
2 | | nfcsb1v 3853 |
. . . 4
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
3 | | csbeq1a 3842 |
. . . 4
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
4 | 1, 2, 3 | cbviun 4962 |
. . 3
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑚 ∈ ℕ
⦋𝑚 / 𝑛⦌𝐴 |
5 | 4 | fveq2i 6742 |
. 2
⊢
(vol*‘∪ 𝑛 ∈ ℕ 𝐴) = (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) |
6 | | ovoliun.a |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) |
7 | | ovoliun.v |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
8 | | ovoliun.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
9 | | 2nn 11933 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
10 | | nnnn0 12127 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
11 | | nnexpcl 13680 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
12 | 9, 10, 11 | sylancr 590 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℕ) |
13 | 12 | nnrpd 12656 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℝ+) |
14 | | rpdivcl 12641 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ+
∧ (2↑𝑛) ∈
ℝ+) → (𝐵 / (2↑𝑛)) ∈
ℝ+) |
15 | 8, 13, 14 | syl2an 599 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 / (2↑𝑛)) ∈
ℝ+) |
16 | | eqid 2739 |
. . . . . . 7
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
17 | 16 | ovolgelb 24409 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ (𝐵 /
(2↑𝑛)) ∈
ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) |
18 | 6, 7, 15, 17 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) |
19 | 18 | ralrimiva 3108 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) |
20 | | ovex 7268 |
. . . . 5
⊢ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ) ∈
V |
21 | | nnenom 13585 |
. . . . 5
⊢ ℕ
≈ ω |
22 | | coeq2 5745 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔‘𝑛) → ((,) ∘ 𝑓) = ((,) ∘ (𝑔‘𝑛))) |
23 | 22 | rneqd 5825 |
. . . . . . . 8
⊢ (𝑓 = (𝑔‘𝑛) → ran ((,) ∘ 𝑓) = ran ((,) ∘ (𝑔‘𝑛))) |
24 | 23 | unieqd 4850 |
. . . . . . 7
⊢ (𝑓 = (𝑔‘𝑛) → ∪ ran
((,) ∘ 𝑓) = ∪ ran ((,) ∘ (𝑔‘𝑛))) |
25 | 24 | sseq2d 3950 |
. . . . . 6
⊢ (𝑓 = (𝑔‘𝑛) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ↔
𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)))) |
26 | | coeq2 5745 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔‘𝑛) → ((abs ∘ − ) ∘
𝑓) = ((abs ∘ −
) ∘ (𝑔‘𝑛))) |
27 | 26 | seqeq3d 13614 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔‘𝑛) → seq1( + , ((abs ∘ − )
∘ 𝑓)) = seq1( + ,
((abs ∘ − ) ∘ (𝑔‘𝑛)))) |
28 | 27 | rneqd 5825 |
. . . . . . . 8
⊢ (𝑓 = (𝑔‘𝑛) → ran seq1( + , ((abs ∘ −
) ∘ 𝑓)) = ran seq1( +
, ((abs ∘ − ) ∘ (𝑔‘𝑛)))) |
29 | 28 | supeq1d 9092 |
. . . . . . 7
⊢ (𝑓 = (𝑔‘𝑛) → sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < ) = sup(ran seq1( + , ((abs ∘ − ) ∘
(𝑔‘𝑛))), ℝ*, <
)) |
30 | 29 | breq1d 5080 |
. . . . . 6
⊢ (𝑓 = (𝑔‘𝑛) → (sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ↔ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) |
31 | 25, 30 | anbi12d 634 |
. . . . 5
⊢ (𝑓 = (𝑔‘𝑛) → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) |
32 | 20, 21, 31 | axcc4 10083 |
. . . 4
⊢
(∀𝑛 ∈
ℕ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) → ∃𝑔(𝑔:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) |
33 | 19, 32 | syl 17 |
. . 3
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) |
34 | | xpnnen 15805 |
. . . . . . 7
⊢ (ℕ
× ℕ) ≈ ℕ |
35 | 34 | ensymi 8704 |
. . . . . 6
⊢ ℕ
≈ (ℕ × ℕ) |
36 | | bren 8660 |
. . . . . 6
⊢ (ℕ
≈ (ℕ × ℕ) ↔ ∃𝑗 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) |
37 | 35, 36 | mpbi 233 |
. . . . 5
⊢
∃𝑗 𝑗:ℕ–1-1-onto→(ℕ × ℕ) |
38 | | ovoliun.t |
. . . . . . . 8
⊢ 𝑇 = seq1( + , 𝐺) |
39 | | ovoliun.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) |
40 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑚(vol*‘𝐴) |
41 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛vol* |
42 | 41, 2 | nffv 6749 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) |
43 | 3 | fveq2d 6743 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (vol*‘𝐴) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
44 | 40, 42, 43 | cbvmpt 5173 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦
(vol*‘𝐴)) = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
45 | 39, 44 | eqtri 2767 |
. . . . . . . 8
⊢ 𝐺 = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
46 | 6 | ralrimiva 3108 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
47 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚 𝐴 ⊆
ℝ |
48 | | nfcv 2907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛ℝ |
49 | 2, 48 | nfss 3909 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ |
50 | 3 | sseq1d 3949 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → (𝐴 ⊆ ℝ ↔ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ)) |
51 | 47, 49, 50 | cbvralw 3364 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ 𝐴 ⊆ ℝ
↔ ∀𝑚 ∈
ℕ ⦋𝑚 /
𝑛⦌𝐴 ⊆
ℝ) |
52 | 46, 51 | sylib 221 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
53 | 52 | r19.21bi 3133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
54 | 53 | ad4ant14 752 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
55 | 7 | ralrimiva 3108 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ (vol*‘𝐴) ∈ ℝ) |
56 | 40 | nfel1 2923 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚(vol*‘𝐴) ∈ ℝ |
57 | 42 | nfel1 2923 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ |
58 | 43 | eleq1d 2824 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((vol*‘𝐴) ∈ ℝ ↔
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ)) |
59 | 56, 57, 58 | cbvralw 3364 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (vol*‘𝐴)
∈ ℝ ↔ ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
60 | 55, 59 | sylib 221 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
61 | 60 | r19.21bi 3133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
62 | 61 | ad4ant14 752 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) →
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
63 | | ovoliun.r |
. . . . . . . . 9
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
64 | 63 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
65 | 8 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → 𝐵 ∈
ℝ+) |
66 | | eqid 2739 |
. . . . . . . 8
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑔‘𝑚))) = seq1( + , ((abs ∘ − )
∘ (𝑔‘𝑚))) |
67 | | eqid 2739 |
. . . . . . . 8
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑘 ∈ ℕ ↦ ((𝑔‘(1st ‘(𝑗‘𝑘)))‘(2nd ‘(𝑗‘𝑘)))))) = seq1( + , ((abs ∘ − )
∘ (𝑘 ∈ ℕ
↦ ((𝑔‘(1st ‘(𝑗‘𝑘)))‘(2nd ‘(𝑗‘𝑘)))))) |
68 | | eqid 2739 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ ↦ ((𝑔‘(1st
‘(𝑗‘𝑘)))‘(2nd
‘(𝑗‘𝑘)))) = (𝑘 ∈ ℕ ↦ ((𝑔‘(1st ‘(𝑗‘𝑘)))‘(2nd ‘(𝑗‘𝑘)))) |
69 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) |
70 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → 𝑔:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)) |
71 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) |
72 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) |
73 | | nfcv 2907 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛∪ ran ((,) ∘ (𝑔‘𝑚)) |
74 | 2, 73 | nfss 3909 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) |
75 | | nfcv 2907 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛sup(ran seq1( + , ((abs ∘ − )
∘ (𝑔‘𝑚))), ℝ*, <
) |
76 | | nfcv 2907 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛
≤ |
77 | | nfcv 2907 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛
+ |
78 | | nfcv 2907 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝐵 / (2↑𝑚)) |
79 | 42, 77, 78 | nfov 7265 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))) |
80 | 75, 76, 79 | nfbr 5117 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛sup(ran
seq1( + , ((abs ∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))) |
81 | 74, 80 | nfan 1907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚)))) |
82 | | fveq2 6739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚)) |
83 | 82 | coeq2d 5749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → ((,) ∘ (𝑔‘𝑛)) = ((,) ∘ (𝑔‘𝑚))) |
84 | 83 | rneqd 5825 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ran ((,) ∘ (𝑔‘𝑛)) = ran ((,) ∘ (𝑔‘𝑚))) |
85 | 84 | unieqd 4850 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ∪ ran ((,)
∘ (𝑔‘𝑛)) = ∪ ran ((,) ∘ (𝑔‘𝑚))) |
86 | 3, 85 | sseq12d 3951 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ↔ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)))) |
87 | 82 | coeq2d 5749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → ((abs ∘ − ) ∘
(𝑔‘𝑛)) = ((abs ∘ − ) ∘ (𝑔‘𝑚))) |
88 | 87 | seqeq3d 13614 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → seq1( + , ((abs ∘ − )
∘ (𝑔‘𝑛))) = seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑚)))) |
89 | 88 | rneqd 5825 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ran seq1( + , ((abs ∘ − )
∘ (𝑔‘𝑛))) = ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚)))) |
90 | 89 | supeq1d 9092 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) = sup(ran
seq1( + , ((abs ∘ − ) ∘ (𝑔‘𝑚))), ℝ*, <
)) |
91 | | oveq2 7243 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚)) |
92 | 91 | oveq2d 7251 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐵 / (2↑𝑛)) = (𝐵 / (2↑𝑚))) |
93 | 43, 92 | oveq12d 7253 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) = ((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚)))) |
94 | 90, 93 | breq12d 5083 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ↔ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))))) |
95 | 86, 94 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ↔ (⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚)))))) |
96 | 72, 81, 95 | cbvralw 3364 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ↔ ∀𝑚 ∈ ℕ (⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))))) |
97 | 71, 96 | sylib 221 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → ∀𝑚 ∈ ℕ (⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))))) |
98 | 97 | r19.21bi 3133 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → (⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))))) |
99 | 98 | simpld 498 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → ⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚))) |
100 | 98 | simprd 499 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → sup(ran seq1( + ,
((abs ∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚)))) |
101 | 38, 45, 54, 62, 64, 65, 66, 67, 68, 69, 70, 99, 100 | ovoliunlem2 24432 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
102 | 101 | exp31 423 |
. . . . . 6
⊢ (𝜑 → (𝑗:ℕ–1-1-onto→(ℕ × ℕ) → ((𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)))) |
103 | 102 | exlimdv 1941 |
. . . . 5
⊢ (𝜑 → (∃𝑗 𝑗:ℕ–1-1-onto→(ℕ × ℕ) → ((𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)))) |
104 | 37, 103 | mpi 20 |
. . . 4
⊢ (𝜑 → ((𝑔:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
105 | 104 | exlimdv 1941 |
. . 3
⊢ (𝜑 → (∃𝑔(𝑔:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
106 | 33, 105 | mpd 15 |
. 2
⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
107 | 5, 106 | eqbrtrid 5105 |
1
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |