Step | Hyp | Ref
| Expression |
1 | | simp2 1062 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (vol*‘𝐴) ∈ ℝ) |
2 | | simp3 1063 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → 𝐵 ∈
ℝ+) |
3 | 1, 2 | ltaddrpd 11905 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (vol*‘𝐴) < ((vol*‘𝐴) + 𝐵)) |
4 | 2 | rpred 11872 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → 𝐵 ∈ ℝ) |
5 | 1, 4 | readdcld 10069 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ((vol*‘𝐴) + 𝐵) ∈ ℝ) |
6 | 1, 5 | ltnled 10184 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ((vol*‘𝐴) < ((vol*‘𝐴) + 𝐵) ↔ ¬ ((vol*‘𝐴) + 𝐵) ≤ (vol*‘𝐴))) |
7 | 3, 6 | mpbid 222 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ¬ ((vol*‘𝐴) + 𝐵) ≤ (vol*‘𝐴)) |
8 | | eqid 2622 |
. . . . . . . 8
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))} = {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))} |
9 | 8 | ovolval 23242 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(vol*‘𝐴) = inf({𝑦 ∈ ℝ*
∣ ∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))}, ℝ*, < )) |
10 | 9 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (vol*‘𝐴) = inf({𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))}, ℝ*, < )) |
11 | 10 | breq2d 4665 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (((vol*‘𝐴) + 𝐵) ≤ (vol*‘𝐴) ↔ ((vol*‘𝐴) + 𝐵) ≤ inf({𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))}, ℝ*, < ))) |
12 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))} ⊆ ℝ* |
13 | 5 | rexrd 10089 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ((vol*‘𝐴) + 𝐵) ∈
ℝ*) |
14 | | infxrgelb 12165 |
. . . . . . 7
⊢ (({𝑦 ∈ ℝ*
∣ ∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))} ⊆ ℝ* ∧
((vol*‘𝐴) + 𝐵) ∈ ℝ*)
→ (((vol*‘𝐴) +
𝐵) ≤ inf({𝑦 ∈ ℝ*
∣ ∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))}, ℝ*, < ) ↔ ∀𝑥 ∈ {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))} ((vol*‘𝐴) + 𝐵) ≤ 𝑥)) |
15 | 12, 13, 14 | sylancr 695 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (((vol*‘𝐴) + 𝐵) ≤ inf({𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))}, ℝ*, < ) ↔ ∀𝑥 ∈ {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))} ((vol*‘𝐴) + 𝐵) ≤ 𝑥)) |
16 | | eqeq1 2626 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ) ↔ 𝑥 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))) |
17 | | ovolgelb.1 |
. . . . . . . . . . . . . 14
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝑔)) |
18 | 17 | rneqi 5352 |
. . . . . . . . . . . . 13
⊢ ran 𝑆 = ran seq1( + , ((abs ∘
− ) ∘ 𝑔)) |
19 | 18 | supeq1i 8353 |
. . . . . . . . . . . 12
⊢ sup(ran
𝑆, ℝ*,
< ) = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑔)), ℝ*, <
) |
20 | 19 | eqeq2i 2634 |
. . . . . . . . . . 11
⊢ (𝑥 = sup(ran 𝑆, ℝ*, < ) ↔ 𝑥 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, <
)) |
21 | 16, 20 | syl6bbr 278 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ) ↔ 𝑥 = sup(ran 𝑆, ℝ*, <
))) |
22 | 21 | anbi2d 740 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < )) ↔
(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, <
)))) |
23 | 22 | rexbidv 3052 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < )) ↔
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, <
)))) |
24 | 23 | ralrab 3368 |
. . . . . . 7
⊢
(∀𝑥 ∈
{𝑦 ∈
ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < ))}
((vol*‘𝐴) + 𝐵) ≤ 𝑥 ↔ ∀𝑥 ∈ ℝ* (∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥)) |
25 | | ralcom 3098 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℝ* ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)∀𝑥 ∈ ℝ* ((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥)) |
26 | | r19.23v 3023 |
. . . . . . . . 9
⊢
(∀𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚
ℕ)((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ (∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥)) |
27 | 26 | ralbii 2980 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℝ* ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ∀𝑥 ∈ ℝ* (∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥)) |
28 | | ancomst 468 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ((𝑥 = sup(ran 𝑆, ℝ*, < ) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝑔)) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥)) |
29 | | impexp 462 |
. . . . . . . . . . . 12
⊢ (((𝑥 = sup(ran 𝑆, ℝ*, < ) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝑔)) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ (𝑥 = sup(ran 𝑆, ℝ*, < ) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥))) |
30 | 28, 29 | bitri 264 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ (𝑥 = sup(ran 𝑆, ℝ*, < ) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥))) |
31 | 30 | ralbii 2980 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
ℝ* ((𝐴
⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ∀𝑥 ∈ ℝ* (𝑥 = sup(ran 𝑆, ℝ*, < ) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥))) |
32 | | reex 10027 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ
∈ V |
33 | 32, 32 | xpex 6962 |
. . . . . . . . . . . . . . . . 17
⊢ (ℝ
× ℝ) ∈ V |
34 | 33 | inex2 4800 |
. . . . . . . . . . . . . . . 16
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
35 | | nnex 11026 |
. . . . . . . . . . . . . . . 16
⊢ ℕ
∈ V |
36 | 34, 35 | elmap 7886 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝑔:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
37 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ ((abs
∘ − ) ∘ 𝑔) = ((abs ∘ − ) ∘ 𝑔) |
38 | 37, 17 | ovolsf 23241 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
39 | 36, 38 | sylbi 207 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → 𝑆:ℕ⟶(0[,)+∞)) |
40 | | frn 6053 |
. . . . . . . . . . . . . 14
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ ran 𝑆 ⊆
(0[,)+∞)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → ran 𝑆 ⊆
(0[,)+∞)) |
42 | | icossxr 12258 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ ℝ* |
43 | 41, 42 | syl6ss 3615 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → ran 𝑆 ⊆
ℝ*) |
44 | | supxrcl 12145 |
. . . . . . . . . . . 12
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → sup(ran 𝑆, ℝ*, < )
∈ ℝ*) |
46 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑥 = sup(ran 𝑆, ℝ*, < ) →
(((vol*‘𝐴) + 𝐵) ≤ 𝑥 ↔ ((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) |
47 | 46 | imbi2d 330 |
. . . . . . . . . . . 12
⊢ (𝑥 = sup(ran 𝑆, ℝ*, < ) → ((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
)))) |
48 | 47 | ceqsralv 3234 |
. . . . . . . . . . 11
⊢ (sup(ran
𝑆, ℝ*,
< ) ∈ ℝ* → (∀𝑥 ∈ ℝ* (𝑥 = sup(ran 𝑆, ℝ*, < ) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥)) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
)))) |
49 | 45, 48 | syl 17 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → (∀𝑥 ∈ ℝ*
(𝑥 = sup(ran 𝑆, ℝ*, < )
→ (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥)) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
)))) |
50 | 31, 49 | syl5bb 272 |
. . . . . . . . 9
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → (∀𝑥 ∈ ℝ*
((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
)))) |
51 | 50 | ralbiia 2979 |
. . . . . . . 8
⊢
(∀𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚
ℕ)∀𝑥 ∈
ℝ* ((𝐴
⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) |
52 | 25, 27, 51 | 3bitr3i 290 |
. . . . . . 7
⊢
(∀𝑥 ∈
ℝ* (∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) |
53 | 24, 52 | bitri 264 |
. . . . . 6
⊢
(∀𝑥 ∈
{𝑦 ∈
ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < ))}
((vol*‘𝐴) + 𝐵) ≤ 𝑥 ↔ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) |
54 | 15, 53 | syl6rbb 277 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < )) ↔
((vol*‘𝐴) + 𝐵) ≤ inf({𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))}, ℝ*, < ))) |
55 | 11, 54 | bitr4d 271 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (((vol*‘𝐴) + 𝐵) ≤ (vol*‘𝐴) ↔ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
)))) |
56 | 7, 55 | mtbid 314 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ¬ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) |
57 | | rexanali 2998 |
. . 3
⊢
(∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ ¬ ((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < )) ↔ ¬
∀𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) |
58 | 56, 57 | sylibr 224 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ ¬
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) |
59 | | xrltnle 10105 |
. . . . . 6
⊢ ((sup(ran
𝑆, ℝ*,
< ) ∈ ℝ* ∧ ((vol*‘𝐴) + 𝐵) ∈ ℝ*) →
(sup(ran 𝑆,
ℝ*, < ) < ((vol*‘𝐴) + 𝐵) ↔ ¬ ((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) |
60 | | xrltle 11982 |
. . . . . 6
⊢ ((sup(ran
𝑆, ℝ*,
< ) ∈ ℝ* ∧ ((vol*‘𝐴) + 𝐵) ∈ ℝ*) →
(sup(ran 𝑆,
ℝ*, < ) < ((vol*‘𝐴) + 𝐵) → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + 𝐵))) |
61 | 59, 60 | sylbird 250 |
. . . . 5
⊢ ((sup(ran
𝑆, ℝ*,
< ) ∈ ℝ* ∧ ((vol*‘𝐴) + 𝐵) ∈ ℝ*) → (¬
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < ) → sup(ran
𝑆, ℝ*,
< ) ≤ ((vol*‘𝐴)
+ 𝐵))) |
62 | 45, 13, 61 | syl2anr 495 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) ∧ 𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) → (¬ ((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < ) → sup(ran
𝑆, ℝ*,
< ) ≤ ((vol*‘𝐴)
+ 𝐵))) |
63 | 62 | anim2d 589 |
. . 3
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) ∧ 𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ ¬
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < )) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + 𝐵)))) |
64 | 63 | reximdva 3017 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ ¬
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < )) →
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + 𝐵)))) |
65 | 58, 64 | mpd 15 |
1
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧
sup(ran 𝑆,
ℝ*, < ) ≤ ((vol*‘𝐴) + 𝐵))) |