Proof of Theorem ovolioo
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ioombl 25600 | . . 3
⊢ (𝐴(,)𝐵) ∈ dom vol | 
| 2 |  | mblvol 25565 | . . 3
⊢ ((𝐴(,)𝐵) ∈ dom vol → (vol‘(𝐴(,)𝐵)) = (vol*‘(𝐴(,)𝐵))) | 
| 3 | 1, 2 | ax-mp 5 | . 2
⊢
(vol‘(𝐴(,)𝐵)) = (vol*‘(𝐴(,)𝐵)) | 
| 4 |  | iccmbl 25601 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol) | 
| 5 |  | mblvol 25565 | . . . . 5
⊢ ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))) | 
| 6 | 4, 5 | syl 17 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))) | 
| 7 | 6 | 3adant3 1133 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))) | 
| 8 | 1 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (𝐴(,)𝐵) ∈ dom vol) | 
| 9 |  | prssi 4821 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → {𝐴, 𝐵} ⊆ ℝ) | 
| 10 | 9 | 3adant3 1133 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → {𝐴, 𝐵} ⊆ ℝ) | 
| 11 |  | prfi 9363 | . . . . . . 7
⊢ {𝐴, 𝐵} ∈ Fin | 
| 12 |  | ovolfi 25529 | . . . . . . 7
⊢ (({𝐴, 𝐵} ∈ Fin ∧ {𝐴, 𝐵} ⊆ ℝ) → (vol*‘{𝐴, 𝐵}) = 0) | 
| 13 | 11, 10, 12 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘{𝐴, 𝐵}) = 0) | 
| 14 |  | nulmbl 25570 | . . . . . 6
⊢ (({𝐴, 𝐵} ⊆ ℝ ∧ (vol*‘{𝐴, 𝐵}) = 0) → {𝐴, 𝐵} ∈ dom vol) | 
| 15 | 10, 13, 14 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → {𝐴, 𝐵} ∈ dom vol) | 
| 16 |  | df-pr 4629 | . . . . . . . 8
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | 
| 17 | 16 | ineq2i 4217 | . . . . . . 7
⊢ ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = ((𝐴(,)𝐵) ∩ ({𝐴} ∪ {𝐵})) | 
| 18 |  | indi 4284 | . . . . . . 7
⊢ ((𝐴(,)𝐵) ∩ ({𝐴} ∪ {𝐵})) = (((𝐴(,)𝐵) ∩ {𝐴}) ∪ ((𝐴(,)𝐵) ∩ {𝐵})) | 
| 19 | 17, 18 | eqtri 2765 | . . . . . 6
⊢ ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = (((𝐴(,)𝐵) ∩ {𝐴}) ∪ ((𝐴(,)𝐵) ∩ {𝐵})) | 
| 20 |  | simp1 1137 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ) | 
| 21 | 20 | ltnrd 11395 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ¬ 𝐴 < 𝐴) | 
| 22 |  | eliooord 13446 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (𝐴(,)𝐵) → (𝐴 < 𝐴 ∧ 𝐴 < 𝐵)) | 
| 23 | 22 | simpld 494 | . . . . . . . . . 10
⊢ (𝐴 ∈ (𝐴(,)𝐵) → 𝐴 < 𝐴) | 
| 24 | 21, 23 | nsyl 140 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ¬ 𝐴 ∈ (𝐴(,)𝐵)) | 
| 25 |  | disjsn 4711 | . . . . . . . . 9
⊢ (((𝐴(,)𝐵) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝐵)) | 
| 26 | 24, 25 | sylibr 234 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∩ {𝐴}) = ∅) | 
| 27 |  | simp2 1138 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ) | 
| 28 | 27 | ltnrd 11395 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ¬ 𝐵 < 𝐵) | 
| 29 |  | eliooord 13446 | . . . . . . . . . . 11
⊢ (𝐵 ∈ (𝐴(,)𝐵) → (𝐴 < 𝐵 ∧ 𝐵 < 𝐵)) | 
| 30 | 29 | simprd 495 | . . . . . . . . . 10
⊢ (𝐵 ∈ (𝐴(,)𝐵) → 𝐵 < 𝐵) | 
| 31 | 28, 30 | nsyl 140 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ¬ 𝐵 ∈ (𝐴(,)𝐵)) | 
| 32 |  | disjsn 4711 | . . . . . . . . 9
⊢ (((𝐴(,)𝐵) ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ (𝐴(,)𝐵)) | 
| 33 | 31, 32 | sylibr 234 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∩ {𝐵}) = ∅) | 
| 34 | 26, 33 | uneq12d 4169 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (((𝐴(,)𝐵) ∩ {𝐴}) ∪ ((𝐴(,)𝐵) ∩ {𝐵})) = (∅ ∪
∅)) | 
| 35 |  | un0 4394 | . . . . . . 7
⊢ (∅
∪ ∅) = ∅ | 
| 36 | 34, 35 | eqtrdi 2793 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (((𝐴(,)𝐵) ∩ {𝐴}) ∪ ((𝐴(,)𝐵) ∩ {𝐵})) = ∅) | 
| 37 | 19, 36 | eqtrid 2789 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = ∅) | 
| 38 |  | ioossicc 13473 | . . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) | 
| 39 |  | iccssre 13469 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) | 
| 40 | 39 | 3adant3 1133 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (𝐴[,]𝐵) ⊆ ℝ) | 
| 41 |  | ovolicc 25558 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)) | 
| 42 | 27, 20 | resubcld 11691 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (𝐵 − 𝐴) ∈ ℝ) | 
| 43 | 41, 42 | eqeltrd 2841 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) ∈ ℝ) | 
| 44 |  | ovolsscl 25521 | . . . . . . 7
⊢ (((𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ (vol*‘(𝐴[,]𝐵)) ∈ ℝ) → (vol*‘(𝐴(,)𝐵)) ∈ ℝ) | 
| 45 | 38, 40, 43, 44 | mp3an2i 1468 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴(,)𝐵)) ∈ ℝ) | 
| 46 | 3, 45 | eqeltrid 2845 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) ∈ ℝ) | 
| 47 |  | mblvol 25565 | . . . . . . . 8
⊢ ({𝐴, 𝐵} ∈ dom vol → (vol‘{𝐴, 𝐵}) = (vol*‘{𝐴, 𝐵})) | 
| 48 | 15, 47 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘{𝐴, 𝐵}) = (vol*‘{𝐴, 𝐵})) | 
| 49 | 48, 13 | eqtrd 2777 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘{𝐴, 𝐵}) = 0) | 
| 50 |  | 0re 11263 | . . . . . 6
⊢ 0 ∈
ℝ | 
| 51 | 49, 50 | eqeltrdi 2849 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘{𝐴, 𝐵}) ∈ ℝ) | 
| 52 |  | volun 25580 | . . . . 5
⊢ ((((𝐴(,)𝐵) ∈ dom vol ∧ {𝐴, 𝐵} ∈ dom vol ∧ ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = ∅) ∧ ((vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ (vol‘{𝐴, 𝐵}) ∈ ℝ)) →
(vol‘((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) = ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴, 𝐵}))) | 
| 53 | 8, 15, 37, 46, 51, 52 | syl32anc 1380 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) = ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴, 𝐵}))) | 
| 54 |  | rexr 11307 | . . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) | 
| 55 |  | rexr 11307 | . . . . . 6
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) | 
| 56 |  | id 22 | . . . . . 6
⊢ (𝐴 ≤ 𝐵 → 𝐴 ≤ 𝐵) | 
| 57 |  | prunioo 13521 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) | 
| 58 | 54, 55, 56, 57 | syl3an 1161 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) | 
| 59 | 58 | fveq2d 6910 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) = (vol‘(𝐴[,]𝐵))) | 
| 60 | 49 | oveq2d 7447 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴, 𝐵})) = ((vol‘(𝐴(,)𝐵)) + 0)) | 
| 61 | 46 | recnd 11289 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) ∈ ℂ) | 
| 62 | 61 | addridd 11461 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((vol‘(𝐴(,)𝐵)) + 0) = (vol‘(𝐴(,)𝐵))) | 
| 63 | 60, 62 | eqtrd 2777 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴, 𝐵})) = (vol‘(𝐴(,)𝐵))) | 
| 64 | 53, 59, 63 | 3eqtr3d 2785 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴[,]𝐵)) = (vol‘(𝐴(,)𝐵))) | 
| 65 | 7, 64, 41 | 3eqtr3d 2785 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) | 
| 66 | 3, 65 | eqtr3id 2791 | 1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |