Step | Hyp | Ref
| Expression |
1 | | elxr 12708 |
. 2
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
2 | | ioossre 12996 |
. . . . 5
⊢ (𝐴(,)+∞) ⊆
ℝ |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℝ → (𝐴(,)+∞) ⊆
ℝ) |
4 | | elpwi 4522 |
. . . . . 6
⊢ (𝑥 ∈ 𝒫 ℝ →
𝑥 ⊆
ℝ) |
5 | | simplrl 777 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) → 𝑥 ⊆ ℝ) |
6 | | simplrr 778 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) → (vol*‘𝑥) ∈ ℝ) |
7 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) → 𝑦 ∈ ℝ+) |
8 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
9 | 8 | ovolgelb 24377 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ ∧ 𝑦 ∈
ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦))) |
10 | 5, 6, 7, 9 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦))) |
11 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐴(,)+∞) = (𝐴(,)+∞) |
12 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝐴 ∈ ℝ) |
13 | 5 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝑥 ⊆ ℝ) |
14 | 6 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → (vol*‘𝑥) ∈
ℝ) |
15 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝑦 ∈ ℝ+) |
16 | | eqid 2737 |
. . . . . . . . . . 11
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑚 ∈ ℕ ↦
〈if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))〉))) = seq1( + , ((abs ∘ −
) ∘ (𝑚 ∈ ℕ
↦ 〈if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))〉))) |
17 | | eqid 2737 |
. . . . . . . . . . 11
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑚 ∈ ℕ ↦ 〈(1st
‘(𝑓‘𝑚)), if(if((1st
‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚)))〉))) = seq1( + , ((abs ∘
− ) ∘ (𝑚 ∈
ℕ ↦ 〈(1st ‘(𝑓‘𝑚)), if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚)))〉))) |
18 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) |
19 | | elovolmlem 24371 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ↔ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
20 | 18, 19 | sylib 221 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
21 | | simprrl 781 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝑥 ⊆ ∪ ran
((,) ∘ 𝑓)) |
22 | | simprrr 782 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → sup(ran seq1( + ,
((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)) |
23 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(1st ‘(𝑓‘𝑛)) = (1st ‘(𝑓‘𝑛)) |
24 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(2nd ‘(𝑓‘𝑛)) = (2nd ‘(𝑓‘𝑛)) |
25 | | 2fveq3 6722 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → (1st ‘(𝑓‘𝑚)) = (1st ‘(𝑓‘𝑛))) |
26 | 25 | breq1d 5063 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑛 → ((1st ‘(𝑓‘𝑚)) ≤ 𝐴 ↔ (1st ‘(𝑓‘𝑛)) ≤ 𝐴)) |
27 | 26, 25 | ifbieq2d 4465 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) = if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛)))) |
28 | | 2fveq3 6722 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (2nd ‘(𝑓‘𝑚)) = (2nd ‘(𝑓‘𝑛))) |
29 | 27, 28 | breq12d 5066 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)) ↔ if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)))) |
30 | 29, 27, 28 | ifbieq12d 4467 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))) = if(if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛)))) |
31 | 30, 28 | opeq12d 4792 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → 〈if(if((1st
‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))〉 = 〈if(if((1st
‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛))〉) |
32 | 31 | cbvmptv 5158 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ ↦
〈if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))〉) = (𝑛 ∈ ℕ ↦
〈if(if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛))〉) |
33 | 25, 30 | opeq12d 4792 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → 〈(1st ‘(𝑓‘𝑚)), if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚)))〉 = 〈(1st
‘(𝑓‘𝑛)), if(if((1st
‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛)))〉) |
34 | 33 | cbvmptv 5158 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ ↦
〈(1st ‘(𝑓‘𝑚)), if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚)))〉) = (𝑛 ∈ ℕ ↦ 〈(1st
‘(𝑓‘𝑛)), if(if((1st
‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛)))〉) |
35 | 11, 12, 13, 14, 15, 8, 16, 17, 20, 21, 22, 23, 24, 32, 34 | ioombl1lem4 24458 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ ((vol*‘𝑥) + 𝑦)) |
36 | 10, 35 | rexlimddv 3210 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ ((vol*‘𝑥) + 𝑦)) |
37 | 36 | ralrimiva 3105 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ∀𝑦
∈ ℝ+ ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ ((vol*‘𝑥) + 𝑦)) |
38 | | inss1 4143 |
. . . . . . . . . . . 12
⊢ (𝑥 ∩ (𝐴(,)+∞)) ⊆ 𝑥 |
39 | | ovolsscl 24383 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∩ (𝐴(,)+∞)) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∩ (𝐴(,)+∞))) ∈
ℝ) |
40 | 38, 39 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ (𝐴(,)+∞))) ∈
ℝ) |
41 | 40 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∩ (𝐴(,)+∞))) ∈
ℝ) |
42 | | difss 4046 |
. . . . . . . . . . . 12
⊢ (𝑥 ∖ (𝐴(,)+∞)) ⊆ 𝑥 |
43 | | ovolsscl 24383 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∖ (𝐴(,)+∞)) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∖
(𝐴(,)+∞))) ∈
ℝ) |
44 | 42, 43 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ (𝐴(,)+∞))) ∈
ℝ) |
45 | 44 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∖ (𝐴(,)+∞))) ∈
ℝ) |
46 | 41, 45 | readdcld 10862 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ∈
ℝ) |
47 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘𝑥) ∈ ℝ) |
48 | | alrple 12796 |
. . . . . . . . 9
⊢
((((vol*‘(𝑥
∩ (𝐴(,)+∞))) +
(vol*‘(𝑥 ∖
(𝐴(,)+∞)))) ∈
ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥) ↔ ∀𝑦 ∈ ℝ+
((vol*‘(𝑥 ∩
(𝐴(,)+∞))) +
(vol*‘(𝑥 ∖
(𝐴(,)+∞)))) ≤
((vol*‘𝑥) + 𝑦))) |
49 | 46, 47, 48 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥) ↔ ∀𝑦 ∈ ℝ+
((vol*‘(𝑥 ∩
(𝐴(,)+∞))) +
(vol*‘(𝑥 ∖
(𝐴(,)+∞)))) ≤
((vol*‘𝑥) + 𝑦))) |
50 | 37, 49 | mpbird 260 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥)) |
51 | 50 | expr 460 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ⊆ ℝ) →
((vol*‘𝑥) ∈
ℝ → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥))) |
52 | 4, 51 | sylan2 596 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝒫 ℝ)
→ ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥))) |
53 | 52 | ralrimiva 3105 |
. . . 4
⊢ (𝐴 ∈ ℝ →
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥))) |
54 | | ismbl2 24424 |
. . . 4
⊢ ((𝐴(,)+∞) ∈ dom vol
↔ ((𝐴(,)+∞)
⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ →
((vol*‘(𝑥 ∩
(𝐴(,)+∞))) +
(vol*‘(𝑥 ∖
(𝐴(,)+∞)))) ≤
(vol*‘𝑥)))) |
55 | 3, 53, 54 | sylanbrc 586 |
. . 3
⊢ (𝐴 ∈ ℝ → (𝐴(,)+∞) ∈ dom
vol) |
56 | | oveq1 7220 |
. . . . 5
⊢ (𝐴 = +∞ → (𝐴(,)+∞) =
(+∞(,)+∞)) |
57 | | iooid 12963 |
. . . . 5
⊢
(+∞(,)+∞) = ∅ |
58 | 56, 57 | eqtrdi 2794 |
. . . 4
⊢ (𝐴 = +∞ → (𝐴(,)+∞) =
∅) |
59 | | 0mbl 24436 |
. . . 4
⊢ ∅
∈ dom vol |
60 | 58, 59 | eqeltrdi 2846 |
. . 3
⊢ (𝐴 = +∞ → (𝐴(,)+∞) ∈ dom
vol) |
61 | | oveq1 7220 |
. . . . 5
⊢ (𝐴 = -∞ → (𝐴(,)+∞) =
(-∞(,)+∞)) |
62 | | ioomax 13010 |
. . . . 5
⊢
(-∞(,)+∞) = ℝ |
63 | 61, 62 | eqtrdi 2794 |
. . . 4
⊢ (𝐴 = -∞ → (𝐴(,)+∞) =
ℝ) |
64 | | rembl 24437 |
. . . 4
⊢ ℝ
∈ dom vol |
65 | 63, 64 | eqeltrdi 2846 |
. . 3
⊢ (𝐴 = -∞ → (𝐴(,)+∞) ∈ dom
vol) |
66 | 55, 60, 65 | 3jaoi 1429 |
. 2
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐴(,)+∞) ∈ dom
vol) |
67 | 1, 66 | sylbi 220 |
1
⊢ (𝐴 ∈ ℝ*
→ (𝐴(,)+∞)
∈ dom vol) |