Proof of Theorem ovolunnul
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1136 | . . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
𝐴 ⊆
ℝ) | 
| 2 |  | simp2 1137 | . . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
𝐵 ⊆
ℝ) | 
| 3 | 1, 2 | unssd 4191 | . . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
(𝐴 ∪ 𝐵) ⊆ ℝ) | 
| 4 |  | ovolcl 25514 | . . 3
⊢ ((𝐴 ∪ 𝐵) ⊆ ℝ → (vol*‘(𝐴 ∪ 𝐵)) ∈
ℝ*) | 
| 5 | 3, 4 | syl 17 | . 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
(vol*‘(𝐴 ∪ 𝐵)) ∈
ℝ*) | 
| 6 |  | ovolcl 25514 | . . 3
⊢ (𝐴 ⊆ ℝ →
(vol*‘𝐴) ∈
ℝ*) | 
| 7 | 6 | 3ad2ant1 1133 | . 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
(vol*‘𝐴) ∈
ℝ*) | 
| 8 |  | xrltnle 11329 | . . . . 5
⊢
(((vol*‘𝐴)
∈ ℝ* ∧ (vol*‘(𝐴 ∪ 𝐵)) ∈ ℝ*) →
((vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵)) ↔ ¬
(vol*‘(𝐴 ∪ 𝐵)) ≤ (vol*‘𝐴))) | 
| 9 | 7, 5, 8 | syl2anc 584 | . . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
((vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵)) ↔ ¬
(vol*‘(𝐴 ∪ 𝐵)) ≤ (vol*‘𝐴))) | 
| 10 | 1 | adantr 480 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → 𝐴 ⊆ ℝ) | 
| 11 |  | mnfxr 11319 | . . . . . . . . 9
⊢ -∞
∈ ℝ* | 
| 12 | 11 | a1i 11 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → -∞ ∈
ℝ*) | 
| 13 | 10, 6 | syl 17 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → (vol*‘𝐴) ∈
ℝ*) | 
| 14 | 5 | adantr 480 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → (vol*‘(𝐴 ∪ 𝐵)) ∈
ℝ*) | 
| 15 |  | ovolge0 25517 | . . . . . . . . . . 11
⊢ (𝐴 ⊆ ℝ → 0 ≤
(vol*‘𝐴)) | 
| 16 | 15 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
0 ≤ (vol*‘𝐴)) | 
| 17 |  | ge0gtmnf 13215 | . . . . . . . . . 10
⊢
(((vol*‘𝐴)
∈ ℝ* ∧ 0 ≤ (vol*‘𝐴)) → -∞ < (vol*‘𝐴)) | 
| 18 | 7, 16, 17 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
-∞ < (vol*‘𝐴)) | 
| 19 | 18 | adantr 480 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → -∞ <
(vol*‘𝐴)) | 
| 20 |  | simpr 484 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → (vol*‘𝐴) < (vol*‘(𝐴 ∪ 𝐵))) | 
| 21 |  | xrre2 13213 | . . . . . . . 8
⊢
(((-∞ ∈ ℝ* ∧ (vol*‘𝐴) ∈ ℝ*
∧ (vol*‘(𝐴 ∪
𝐵)) ∈
ℝ*) ∧ (-∞ < (vol*‘𝐴) ∧ (vol*‘𝐴) < (vol*‘(𝐴 ∪ 𝐵)))) → (vol*‘𝐴) ∈ ℝ) | 
| 22 | 12, 13, 14, 19, 20, 21 | syl32anc 1379 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → (vol*‘𝐴) ∈
ℝ) | 
| 23 | 2 | adantr 480 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → 𝐵 ⊆ ℝ) | 
| 24 |  | simpl3 1193 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → (vol*‘𝐵) = 0) | 
| 25 |  | 0re 11264 | . . . . . . . 8
⊢ 0 ∈
ℝ | 
| 26 | 24, 25 | eqeltrdi 2848 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → (vol*‘𝐵) ∈
ℝ) | 
| 27 |  | ovolun 25535 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (𝐵 ⊆
ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) | 
| 28 | 10, 22, 23, 26, 27 | syl22anc 838 | . . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) | 
| 29 | 24 | oveq2d 7448 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → ((vol*‘𝐴) + (vol*‘𝐵)) = ((vol*‘𝐴) + 0)) | 
| 30 | 22 | recnd 11290 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → (vol*‘𝐴) ∈
ℂ) | 
| 31 | 30 | addridd 11462 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → ((vol*‘𝐴) + 0) = (vol*‘𝐴)) | 
| 32 | 29, 31 | eqtrd 2776 | . . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → ((vol*‘𝐴) + (vol*‘𝐵)) = (vol*‘𝐴)) | 
| 33 | 28, 32 | breqtrd 5168 | . . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) ∧
(vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵))) → (vol*‘(𝐴 ∪ 𝐵)) ≤ (vol*‘𝐴)) | 
| 34 | 33 | ex 412 | . . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
((vol*‘𝐴) <
(vol*‘(𝐴 ∪ 𝐵)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ (vol*‘𝐴))) | 
| 35 | 9, 34 | sylbird 260 | . . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
(¬ (vol*‘(𝐴 ∪
𝐵)) ≤ (vol*‘𝐴) → (vol*‘(𝐴 ∪ 𝐵)) ≤ (vol*‘𝐴))) | 
| 36 | 35 | pm2.18d 127 | . 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
(vol*‘(𝐴 ∪ 𝐵)) ≤ (vol*‘𝐴)) | 
| 37 |  | ssun1 4177 | . . 3
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) | 
| 38 |  | ovolss 25521 | . . 3
⊢ ((𝐴 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘(𝐴 ∪ 𝐵))) | 
| 39 | 37, 3, 38 | sylancr 587 | . 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
(vol*‘𝐴) ≤
(vol*‘(𝐴 ∪ 𝐵))) | 
| 40 | 5, 7, 36, 39 | xrletrid 13198 | 1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
(vol*‘𝐵) = 0) →
(vol*‘(𝐴 ∪ 𝐵)) = (vol*‘𝐴)) |