| Step | Hyp | Ref
| Expression |
| 1 | | ovolsca.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐴 ⊆
ℝ) |
| 3 | | ovolsca.4 |
. . . . . 6
⊢ (𝜑 → (vol*‘𝐴) ∈
ℝ) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(vol*‘𝐴) ∈
ℝ) |
| 5 | | ovolsca.2 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
| 6 | | rpmulcl 13058 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ+
∧ 𝑦 ∈
ℝ+) → (𝐶 · 𝑦) ∈
ℝ+) |
| 7 | 5, 6 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝐶 · 𝑦) ∈
ℝ+) |
| 8 | | eqid 2737 |
. . . . . 6
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
| 9 | 8 | ovolgelb 25515 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ (𝐶 ·
𝑦) ∈
ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦)))) |
| 10 | 2, 4, 7, 9 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦)))) |
| 11 | 1 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦))))) → 𝐴 ⊆ ℝ) |
| 12 | 5 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦))))) → 𝐶 ∈
ℝ+) |
| 13 | | ovolsca.3 |
. . . . . 6
⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) |
| 14 | 13 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦))))) → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) |
| 15 | 3 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦))))) → (vol*‘𝐴) ∈ ℝ) |
| 16 | | 2fveq3 6911 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (1st ‘(𝑓‘𝑚)) = (1st ‘(𝑓‘𝑛))) |
| 17 | 16 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → ((1st ‘(𝑓‘𝑚)) / 𝐶) = ((1st ‘(𝑓‘𝑛)) / 𝐶)) |
| 18 | | 2fveq3 6911 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (2nd ‘(𝑓‘𝑚)) = (2nd ‘(𝑓‘𝑛))) |
| 19 | 18 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → ((2nd ‘(𝑓‘𝑚)) / 𝐶) = ((2nd ‘(𝑓‘𝑛)) / 𝐶)) |
| 20 | 17, 19 | opeq12d 4881 |
. . . . . 6
⊢ (𝑚 = 𝑛 → 〈((1st ‘(𝑓‘𝑚)) / 𝐶), ((2nd ‘(𝑓‘𝑚)) / 𝐶)〉 = 〈((1st
‘(𝑓‘𝑛)) / 𝐶), ((2nd ‘(𝑓‘𝑛)) / 𝐶)〉) |
| 21 | 20 | cbvmptv 5255 |
. . . . 5
⊢ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) / 𝐶), ((2nd ‘(𝑓‘𝑚)) / 𝐶)〉) = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑛)) / 𝐶), ((2nd ‘(𝑓‘𝑛)) / 𝐶)〉) |
| 22 | | elmapi 8889 |
. . . . . 6
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
| 23 | 22 | ad2antrl 728 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦))))) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
| 24 | | simprrl 781 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦))))) → 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) |
| 25 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦))))) → 𝑦 ∈ ℝ+) |
| 26 | | simprrr 782 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦))))) → sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑦))) |
| 27 | 11, 12, 14, 15, 8, 21, 23, 24, 25, 26 | ovolscalem1 25548 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑦))))) → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑦)) |
| 28 | 10, 27 | rexlimddv 3161 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(vol*‘𝐵) ≤
(((vol*‘𝐴) / 𝐶) + 𝑦)) |
| 29 | 28 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑦)) |
| 30 | | ssrab2 4080 |
. . . . 5
⊢ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ⊆ ℝ |
| 31 | 13, 30 | eqsstrdi 4028 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
| 32 | | ovolcl 25513 |
. . . 4
⊢ (𝐵 ⊆ ℝ →
(vol*‘𝐵) ∈
ℝ*) |
| 33 | 31, 32 | syl 17 |
. . 3
⊢ (𝜑 → (vol*‘𝐵) ∈
ℝ*) |
| 34 | 3, 5 | rerpdivcld 13108 |
. . 3
⊢ (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℝ) |
| 35 | | xralrple 13247 |
. . 3
⊢
(((vol*‘𝐵)
∈ ℝ* ∧ ((vol*‘𝐴) / 𝐶) ∈ ℝ) → ((vol*‘𝐵) ≤ ((vol*‘𝐴) / 𝐶) ↔ ∀𝑦 ∈ ℝ+ (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑦))) |
| 36 | 33, 34, 35 | syl2anc 584 |
. 2
⊢ (𝜑 → ((vol*‘𝐵) ≤ ((vol*‘𝐴) / 𝐶) ↔ ∀𝑦 ∈ ℝ+ (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑦))) |
| 37 | 29, 36 | mpbird 257 |
1
⊢ (𝜑 → (vol*‘𝐵) ≤ ((vol*‘𝐴) / 𝐶)) |