Step | Hyp | Ref
| Expression |
1 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑚𝐴 |
2 | | nfcsb1v 3515 |
. . . 4
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
3 | | csbeq1a 3508 |
. . . 4
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
4 | 1, 2, 3 | cbviun 4493 |
. . 3
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑚 ∈ ℕ
⦋𝑚 / 𝑛⦌𝐴 |
5 | 4 | fveq2i 6106 |
. 2
⊢
(vol*‘∪ 𝑛 ∈ ℕ 𝐴) = (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) |
6 | | ovoliun.a |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) |
7 | | ovoliun.v |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
8 | | ovoliun.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
9 | | 2nn 11062 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
10 | | nnnn0 11176 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
11 | | nnexpcl 12735 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
12 | 9, 10, 11 | sylancr 694 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℕ) |
13 | 12 | nnrpd 11746 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℝ+) |
14 | | rpdivcl 11732 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ+
∧ (2↑𝑛) ∈
ℝ+) → (𝐵 / (2↑𝑛)) ∈
ℝ+) |
15 | 8, 13, 14 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 / (2↑𝑛)) ∈
ℝ+) |
16 | | eqid 2610 |
. . . . . . 7
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
17 | 16 | ovolgelb 23055 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ (𝐵 /
(2↑𝑛)) ∈
ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) |
18 | 6, 7, 15, 17 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) |
19 | 18 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) |
20 | | ovex 6577 |
. . . . 5
⊢ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ) ∈
V |
21 | | nnenom 12641 |
. . . . 5
⊢ ℕ
≈ ω |
22 | | coeq2 5202 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔‘𝑛) → ((,) ∘ 𝑓) = ((,) ∘ (𝑔‘𝑛))) |
23 | 22 | rneqd 5274 |
. . . . . . . 8
⊢ (𝑓 = (𝑔‘𝑛) → ran ((,) ∘ 𝑓) = ran ((,) ∘ (𝑔‘𝑛))) |
24 | 23 | unieqd 4382 |
. . . . . . 7
⊢ (𝑓 = (𝑔‘𝑛) → ∪ ran
((,) ∘ 𝑓) = ∪ ran ((,) ∘ (𝑔‘𝑛))) |
25 | 24 | sseq2d 3596 |
. . . . . 6
⊢ (𝑓 = (𝑔‘𝑛) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ↔
𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)))) |
26 | | coeq2 5202 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔‘𝑛) → ((abs ∘ − ) ∘
𝑓) = ((abs ∘ −
) ∘ (𝑔‘𝑛))) |
27 | 26 | seqeq3d 12671 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔‘𝑛) → seq1( + , ((abs ∘ − )
∘ 𝑓)) = seq1( + ,
((abs ∘ − ) ∘ (𝑔‘𝑛)))) |
28 | 27 | rneqd 5274 |
. . . . . . . 8
⊢ (𝑓 = (𝑔‘𝑛) → ran seq1( + , ((abs ∘ −
) ∘ 𝑓)) = ran seq1( +
, ((abs ∘ − ) ∘ (𝑔‘𝑛)))) |
29 | 28 | supeq1d 8235 |
. . . . . . 7
⊢ (𝑓 = (𝑔‘𝑛) → sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < ) = sup(ran seq1( + , ((abs ∘ − ) ∘
(𝑔‘𝑛))), ℝ*, <
)) |
30 | 29 | breq1d 4593 |
. . . . . 6
⊢ (𝑓 = (𝑔‘𝑛) → (sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ↔ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) |
31 | 25, 30 | anbi12d 743 |
. . . . 5
⊢ (𝑓 = (𝑔‘𝑛) → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) |
32 | 20, 21, 31 | axcc4 9144 |
. . . 4
⊢
(∀𝑛 ∈
ℕ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) → ∃𝑔(𝑔:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) |
33 | 19, 32 | syl 17 |
. . 3
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) |
34 | | xpnnen 14778 |
. . . . . . 7
⊢ (ℕ
× ℕ) ≈ ℕ |
35 | 34 | ensymi 7892 |
. . . . . 6
⊢ ℕ
≈ (ℕ × ℕ) |
36 | | bren 7850 |
. . . . . 6
⊢ (ℕ
≈ (ℕ × ℕ) ↔ ∃𝑗 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) |
37 | 35, 36 | mpbi 219 |
. . . . 5
⊢
∃𝑗 𝑗:ℕ–1-1-onto→(ℕ × ℕ) |
38 | | ovoliun.t |
. . . . . . . 8
⊢ 𝑇 = seq1( + , 𝐺) |
39 | | ovoliun.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) |
40 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑚(vol*‘𝐴) |
41 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛vol* |
42 | 41, 2 | nffv 6110 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) |
43 | 3 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (vol*‘𝐴) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
44 | 40, 42, 43 | cbvmpt 4677 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦
(vol*‘𝐴)) = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
45 | 39, 44 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐺 = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
46 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → 𝜑) |
47 | 6 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
48 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚 𝐴 ⊆
ℝ |
49 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛ℝ |
50 | 2, 49 | nfss 3561 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ |
51 | 3 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → (𝐴 ⊆ ℝ ↔ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ)) |
52 | 48, 50, 51 | cbvral 3143 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ 𝐴 ⊆ ℝ
↔ ∀𝑚 ∈
ℕ ⦋𝑚 /
𝑛⦌𝐴 ⊆
ℝ) |
53 | 47, 52 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
54 | 53 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
55 | 46, 54 | sylan 487 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
56 | 7 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ (vol*‘𝐴) ∈ ℝ) |
57 | 40 | nfel1 2765 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚(vol*‘𝐴) ∈ ℝ |
58 | 42 | nfel1 2765 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ |
59 | 43 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((vol*‘𝐴) ∈ ℝ ↔
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ)) |
60 | 57, 58, 59 | cbvral 3143 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (vol*‘𝐴)
∈ ℝ ↔ ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
61 | 56, 60 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
62 | 61 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
63 | 46, 62 | sylan 487 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) →
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
64 | | ovoliun.r |
. . . . . . . . 9
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
65 | 64 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
66 | 8 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → 𝐵 ∈
ℝ+) |
67 | | eqid 2610 |
. . . . . . . 8
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑔‘𝑚))) = seq1( + , ((abs ∘ − )
∘ (𝑔‘𝑚))) |
68 | | eqid 2610 |
. . . . . . . 8
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑘 ∈ ℕ ↦ ((𝑔‘(1st ‘(𝑗‘𝑘)))‘(2nd ‘(𝑗‘𝑘)))))) = seq1( + , ((abs ∘ − )
∘ (𝑘 ∈ ℕ
↦ ((𝑔‘(1st ‘(𝑗‘𝑘)))‘(2nd ‘(𝑗‘𝑘)))))) |
69 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ ↦ ((𝑔‘(1st
‘(𝑗‘𝑘)))‘(2nd
‘(𝑗‘𝑘)))) = (𝑘 ∈ ℕ ↦ ((𝑔‘(1st ‘(𝑗‘𝑘)))‘(2nd ‘(𝑗‘𝑘)))) |
70 | | simplr 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) |
71 | | simprl 790 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → 𝑔:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)) |
72 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) |
73 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) |
74 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛∪ ran ((,) ∘ (𝑔‘𝑚)) |
75 | 2, 74 | nfss 3561 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) |
76 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛sup(ran seq1( + , ((abs ∘ − )
∘ (𝑔‘𝑚))), ℝ*, <
) |
77 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛
≤ |
78 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛
+ |
79 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝐵 / (2↑𝑚)) |
80 | 42, 78, 79 | nfov 6575 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))) |
81 | 76, 77, 80 | nfbr 4629 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛sup(ran
seq1( + , ((abs ∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))) |
82 | 75, 81 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚)))) |
83 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚)) |
84 | 83 | coeq2d 5206 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → ((,) ∘ (𝑔‘𝑛)) = ((,) ∘ (𝑔‘𝑚))) |
85 | 84 | rneqd 5274 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ran ((,) ∘ (𝑔‘𝑛)) = ran ((,) ∘ (𝑔‘𝑚))) |
86 | 85 | unieqd 4382 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ∪ ran ((,)
∘ (𝑔‘𝑛)) = ∪ ran ((,) ∘ (𝑔‘𝑚))) |
87 | 3, 86 | sseq12d 3597 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ↔ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)))) |
88 | 83 | coeq2d 5206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → ((abs ∘ − ) ∘
(𝑔‘𝑛)) = ((abs ∘ − ) ∘ (𝑔‘𝑚))) |
89 | 88 | seqeq3d 12671 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → seq1( + , ((abs ∘ − )
∘ (𝑔‘𝑛))) = seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑚)))) |
90 | 89 | rneqd 5274 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ran seq1( + , ((abs ∘ − )
∘ (𝑔‘𝑛))) = ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚)))) |
91 | 90 | supeq1d 8235 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) = sup(ran
seq1( + , ((abs ∘ − ) ∘ (𝑔‘𝑚))), ℝ*, <
)) |
92 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚)) |
93 | 92 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐵 / (2↑𝑛)) = (𝐵 / (2↑𝑚))) |
94 | 43, 93 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) = ((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚)))) |
95 | 91, 94 | breq12d 4596 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ↔ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))))) |
96 | 87, 95 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ↔ (⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚)))))) |
97 | 73, 82, 96 | cbvral 3143 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ↔ ∀𝑚 ∈ ℕ (⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))))) |
98 | 72, 97 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → ∀𝑚 ∈ ℕ (⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))))) |
99 | 98 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → (⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚)) ∧ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚))))) |
100 | 99 | simpld 474 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → ⦋𝑚 / 𝑛⦌𝐴 ⊆ ∪ ran
((,) ∘ (𝑔‘𝑚))) |
101 | 99 | simprd 478 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → sup(ran seq1( + ,
((abs ∘ − ) ∘ (𝑔‘𝑚))), ℝ*, < ) ≤
((vol*‘⦋𝑚 / 𝑛⦌𝐴) + (𝐵 / (2↑𝑚)))) |
102 | 38, 45, 55, 63, 65, 66, 67, 68, 69, 70, 71, 100, 101 | ovoliunlem2 23078 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
103 | 102 | exp31 628 |
. . . . . 6
⊢ (𝜑 → (𝑗:ℕ–1-1-onto→(ℕ × ℕ) → ((𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)))) |
104 | 103 | exlimdv 1848 |
. . . . 5
⊢ (𝜑 → (∃𝑗 𝑗:ℕ–1-1-onto→(ℕ × ℕ) → ((𝑔:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧
∀𝑛 ∈ ℕ
(𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)))) |
105 | 37, 104 | mpi 20 |
. . . 4
⊢ (𝜑 → ((𝑔:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
106 | 105 | exlimdv 1848 |
. . 3
⊢ (𝜑 → (∃𝑔(𝑔:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ⊆ ∪ ran ((,) ∘ (𝑔‘𝑛)) ∧ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑔‘𝑛))), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))) |
107 | 33, 106 | mpd 15 |
. 2
⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
108 | 5, 107 | syl5eqbr 4618 |
1
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |