| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp2 1138 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (vol*‘𝐴) ∈ ℝ) | 
| 2 |  | simp3 1139 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → 𝐵 ∈
ℝ+) | 
| 3 | 1, 2 | ltaddrpd 13110 | . . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (vol*‘𝐴) < ((vol*‘𝐴) + 𝐵)) | 
| 4 | 2 | rpred 13077 | . . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → 𝐵 ∈ ℝ) | 
| 5 | 1, 4 | readdcld 11290 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ((vol*‘𝐴) + 𝐵) ∈ ℝ) | 
| 6 | 1, 5 | ltnled 11408 | . . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ((vol*‘𝐴) < ((vol*‘𝐴) + 𝐵) ↔ ¬ ((vol*‘𝐴) + 𝐵) ≤ (vol*‘𝐴))) | 
| 7 | 3, 6 | mpbid 232 | . . . 4
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ¬ ((vol*‘𝐴) + 𝐵) ≤ (vol*‘𝐴)) | 
| 8 |  | eqid 2737 | . . . . . . . 8
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))} = {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, <
))} | 
| 9 | 8 | ovolval 25508 | . . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(vol*‘𝐴) = inf({𝑦 ∈ ℝ*
∣ ∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))}, ℝ*, < )) | 
| 10 | 9 | 3ad2ant1 1134 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (vol*‘𝐴) = inf({𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < ))},
ℝ*, < )) | 
| 11 | 10 | breq2d 5155 | . . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (((vol*‘𝐴) + 𝐵) ≤ (vol*‘𝐴) ↔ ((vol*‘𝐴) + 𝐵) ≤ inf({𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < ))},
ℝ*, < ))) | 
| 12 |  | ssrab2 4080 | . . . . . . 7
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))} ⊆ ℝ* | 
| 13 | 5 | rexrd 11311 | . . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ((vol*‘𝐴) + 𝐵) ∈
ℝ*) | 
| 14 |  | infxrgelb 13377 | . . . . . . 7
⊢ (({𝑦 ∈ ℝ*
∣ ∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))} ⊆ ℝ* ∧
((vol*‘𝐴) + 𝐵) ∈ ℝ*)
→ (((vol*‘𝐴) +
𝐵) ≤ inf({𝑦 ∈ ℝ*
∣ ∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))}, ℝ*, < ) ↔ ∀𝑥 ∈ {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < ))}
((vol*‘𝐴) + 𝐵) ≤ 𝑥)) | 
| 15 | 12, 13, 14 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (((vol*‘𝐴) + 𝐵) ≤ inf({𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < ))},
ℝ*, < ) ↔ ∀𝑥 ∈ {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < ))}
((vol*‘𝐴) + 𝐵) ≤ 𝑥)) | 
| 16 |  | eqeq1 2741 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ) ↔ 𝑥 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ))) | 
| 17 |  | ovolgelb.1 | . . . . . . . . . . . . . 14
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝑔)) | 
| 18 | 17 | rneqi 5948 | . . . . . . . . . . . . 13
⊢ ran 𝑆 = ran seq1( + , ((abs ∘
− ) ∘ 𝑔)) | 
| 19 | 18 | supeq1i 9487 | . . . . . . . . . . . 12
⊢ sup(ran
𝑆, ℝ*,
< ) = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑔)), ℝ*, <
) | 
| 20 | 19 | eqeq2i 2750 | . . . . . . . . . . 11
⊢ (𝑥 = sup(ran 𝑆, ℝ*, < ) ↔ 𝑥 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, <
)) | 
| 21 | 16, 20 | bitr4di 289 | . . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑔)),
ℝ*, < ) ↔ 𝑥 = sup(ran 𝑆, ℝ*, <
))) | 
| 22 | 21 | anbi2d 630 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < )) ↔
(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, <
)))) | 
| 23 | 22 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → (∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < )) ↔
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, <
)))) | 
| 24 | 23 | ralrab 3699 | . . . . . . 7
⊢
(∀𝑥 ∈
{𝑦 ∈
ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < ))}
((vol*‘𝐴) + 𝐵) ≤ 𝑥 ↔ ∀𝑥 ∈ ℝ* (∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥)) | 
| 25 |  | ralcom 3289 | . . . . . . . 8
⊢
(∀𝑥 ∈
ℝ* ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)∀𝑥 ∈ ℝ* ((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥)) | 
| 26 |  | r19.23v 3183 | . . . . . . . . 9
⊢
(∀𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ (∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥)) | 
| 27 | 26 | ralbii 3093 | . . . . . . . 8
⊢
(∀𝑥 ∈
ℝ* ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ∀𝑥 ∈ ℝ* (∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥)) | 
| 28 |  | ancomst 464 | . . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ((𝑥 = sup(ran 𝑆, ℝ*, < ) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝑔)) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥)) | 
| 29 |  | impexp 450 | . . . . . . . . . . . 12
⊢ (((𝑥 = sup(ran 𝑆, ℝ*, < ) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝑔)) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ (𝑥 = sup(ran 𝑆, ℝ*, < ) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥))) | 
| 30 | 28, 29 | bitri 275 | . . . . . . . . . . 11
⊢ (((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ (𝑥 = sup(ran 𝑆, ℝ*, < ) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥))) | 
| 31 | 30 | ralbii 3093 | . . . . . . . . . 10
⊢
(∀𝑥 ∈
ℝ* ((𝐴
⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ∀𝑥 ∈ ℝ* (𝑥 = sup(ran 𝑆, ℝ*, < ) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥))) | 
| 32 |  | elovolmlem 25509 | . . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ↔ 𝑔:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) | 
| 33 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢ ((abs
∘ − ) ∘ 𝑔) = ((abs ∘ − ) ∘ 𝑔) | 
| 34 | 33, 17 | ovolsf 25507 | . . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) | 
| 35 | 32, 34 | sylbi 217 | . . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 𝑆:ℕ⟶(0[,)+∞)) | 
| 36 | 35 | frnd 6744 | . . . . . . . . . . . . 13
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → ran 𝑆 ⊆ (0[,)+∞)) | 
| 37 |  | icossxr 13472 | . . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ ℝ* | 
| 38 | 36, 37 | sstrdi 3996 | . . . . . . . . . . . 12
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → ran 𝑆 ⊆
ℝ*) | 
| 39 |  | supxrcl 13357 | . . . . . . . . . . . 12
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) | 
| 40 | 38, 39 | syl 17 | . . . . . . . . . . 11
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) | 
| 41 |  | breq2 5147 | . . . . . . . . . . . . 13
⊢ (𝑥 = sup(ran 𝑆, ℝ*, < ) →
(((vol*‘𝐴) + 𝐵) ≤ 𝑥 ↔ ((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) | 
| 42 | 41 | imbi2d 340 | . . . . . . . . . . . 12
⊢ (𝑥 = sup(ran 𝑆, ℝ*, < ) → ((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
)))) | 
| 43 | 42 | ceqsralv 3522 | . . . . . . . . . . 11
⊢ (sup(ran
𝑆, ℝ*,
< ) ∈ ℝ* → (∀𝑥 ∈ ℝ* (𝑥 = sup(ran 𝑆, ℝ*, < ) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥)) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
)))) | 
| 44 | 40, 43 | syl 17 | . . . . . . . . . 10
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → (∀𝑥 ∈ ℝ*
(𝑥 = sup(ran 𝑆, ℝ*, < )
→ (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) → ((vol*‘𝐴) + 𝐵) ≤ 𝑥)) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
)))) | 
| 45 | 31, 44 | bitrid 283 | . . . . . . . . 9
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → (∀𝑥 ∈ ℝ*
((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
)))) | 
| 46 | 45 | ralbiia 3091 | . . . . . . . 8
⊢
(∀𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)∀𝑥 ∈ ℝ*
((𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) | 
| 47 | 25, 27, 46 | 3bitr3i 301 | . . . . . . 7
⊢
(∀𝑥 ∈
ℝ* (∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑥 = sup(ran 𝑆, ℝ*, < )) →
((vol*‘𝐴) + 𝐵) ≤ 𝑥) ↔ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) | 
| 48 | 24, 47 | bitri 275 | . . . . . 6
⊢
(∀𝑥 ∈
{𝑦 ∈
ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < ))}
((vol*‘𝐴) + 𝐵) ≤ 𝑥 ↔ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) | 
| 49 | 15, 48 | bitr2di 288 | . . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < )) ↔
((vol*‘𝐴) + 𝐵) ≤ inf({𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑔)), ℝ*, < ))},
ℝ*, < ))) | 
| 50 | 11, 49 | bitr4d 282 | . . . 4
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (((vol*‘𝐴) + 𝐵) ≤ (vol*‘𝐴) ↔ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
)))) | 
| 51 | 7, 50 | mtbid 324 | . . 3
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ¬ ∀𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) | 
| 52 |  | rexanali 3102 | . . 3
⊢
(∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ ¬ ((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < )) ↔ ¬
∀𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) →
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) | 
| 53 | 51, 52 | sylibr 234 | . 2
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ ¬
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) | 
| 54 |  | xrltnle 11328 | . . . . . 6
⊢ ((sup(ran
𝑆, ℝ*,
< ) ∈ ℝ* ∧ ((vol*‘𝐴) + 𝐵) ∈ ℝ*) →
(sup(ran 𝑆,
ℝ*, < ) < ((vol*‘𝐴) + 𝐵) ↔ ¬ ((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, <
))) | 
| 55 |  | xrltle 13191 | . . . . . 6
⊢ ((sup(ran
𝑆, ℝ*,
< ) ∈ ℝ* ∧ ((vol*‘𝐴) + 𝐵) ∈ ℝ*) →
(sup(ran 𝑆,
ℝ*, < ) < ((vol*‘𝐴) + 𝐵) → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + 𝐵))) | 
| 56 | 54, 55 | sylbird 260 | . . . . 5
⊢ ((sup(ran
𝑆, ℝ*,
< ) ∈ ℝ* ∧ ((vol*‘𝐴) + 𝐵) ∈ ℝ*) → (¬
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < ) → sup(ran
𝑆, ℝ*,
< ) ≤ ((vol*‘𝐴)
+ 𝐵))) | 
| 57 | 40, 13, 56 | syl2anr 597 | . . . 4
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) ∧ 𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) → (¬ ((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < ) → sup(ran
𝑆, ℝ*,
< ) ≤ ((vol*‘𝐴)
+ 𝐵))) | 
| 58 | 57 | anim2d 612 | . . 3
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) ∧ 𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ ¬
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < )) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + 𝐵)))) | 
| 59 | 58 | reximdva 3168 | . 2
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → (∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ ¬
((vol*‘𝐴) + 𝐵) ≤ sup(ran 𝑆, ℝ*, < )) →
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧
sup(ran 𝑆,
ℝ*, < ) ≤ ((vol*‘𝐴) + 𝐵)))) | 
| 60 | 53, 59 | mpd 15 | 1
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℝ+) → ∃𝑔 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧
sup(ran 𝑆,
ℝ*, < ) ≤ ((vol*‘𝐴) + 𝐵))) |