| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ioombl |
⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol |
| 2 |
|
mblvol |
⊢ ( ( 𝐴 (,) 𝐵 ) ∈ dom vol → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ) |
| 3 |
1 2
|
ax-mp |
⊢ ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) |
| 4 |
|
iccmbl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ∈ dom vol ) |
| 5 |
|
mblvol |
⊢ ( ( 𝐴 [,] 𝐵 ) ∈ dom vol → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ) |
| 6 |
4 5
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ) |
| 7 |
6
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ) |
| 8 |
1
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 (,) 𝐵 ) ∈ dom vol ) |
| 9 |
|
prssi |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { 𝐴 , 𝐵 } ⊆ ℝ ) |
| 10 |
9
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → { 𝐴 , 𝐵 } ⊆ ℝ ) |
| 11 |
|
prfi |
⊢ { 𝐴 , 𝐵 } ∈ Fin |
| 12 |
|
ovolfi |
⊢ ( ( { 𝐴 , 𝐵 } ∈ Fin ∧ { 𝐴 , 𝐵 } ⊆ ℝ ) → ( vol* ‘ { 𝐴 , 𝐵 } ) = 0 ) |
| 13 |
11 10 12
|
sylancr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ { 𝐴 , 𝐵 } ) = 0 ) |
| 14 |
|
nulmbl |
⊢ ( ( { 𝐴 , 𝐵 } ⊆ ℝ ∧ ( vol* ‘ { 𝐴 , 𝐵 } ) = 0 ) → { 𝐴 , 𝐵 } ∈ dom vol ) |
| 15 |
10 13 14
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → { 𝐴 , 𝐵 } ∈ dom vol ) |
| 16 |
|
df-pr |
⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } ) |
| 17 |
16
|
ineq2i |
⊢ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ( ( 𝐴 (,) 𝐵 ) ∩ ( { 𝐴 } ∪ { 𝐵 } ) ) |
| 18 |
|
indi |
⊢ ( ( 𝐴 (,) 𝐵 ) ∩ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 } ) ∪ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐵 } ) ) |
| 19 |
17 18
|
eqtri |
⊢ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ( ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 } ) ∪ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐵 } ) ) |
| 20 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ ) |
| 21 |
20
|
ltnrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ¬ 𝐴 < 𝐴 ) |
| 22 |
|
eliooord |
⊢ ( 𝐴 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝐴 ∧ 𝐴 < 𝐵 ) ) |
| 23 |
22
|
simpld |
⊢ ( 𝐴 ∈ ( 𝐴 (,) 𝐵 ) → 𝐴 < 𝐴 ) |
| 24 |
21 23
|
nsyl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ¬ 𝐴 ∈ ( 𝐴 (,) 𝐵 ) ) |
| 25 |
|
disjsn |
⊢ ( ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ ( 𝐴 (,) 𝐵 ) ) |
| 26 |
24 25
|
sylibr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 } ) = ∅ ) |
| 27 |
|
simp2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ ) |
| 28 |
27
|
ltnrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ¬ 𝐵 < 𝐵 ) |
| 29 |
|
eliooord |
⊢ ( 𝐵 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐵 ) ) |
| 30 |
29
|
simprd |
⊢ ( 𝐵 ∈ ( 𝐴 (,) 𝐵 ) → 𝐵 < 𝐵 ) |
| 31 |
28 30
|
nsyl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ¬ 𝐵 ∈ ( 𝐴 (,) 𝐵 ) ) |
| 32 |
|
disjsn |
⊢ ( ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ ( 𝐴 (,) 𝐵 ) ) |
| 33 |
31 32
|
sylibr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐵 } ) = ∅ ) |
| 34 |
26 33
|
uneq12d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 } ) ∪ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐵 } ) ) = ( ∅ ∪ ∅ ) ) |
| 35 |
|
un0 |
⊢ ( ∅ ∪ ∅ ) = ∅ |
| 36 |
34 35
|
eqtrdi |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 } ) ∪ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐵 } ) ) = ∅ ) |
| 37 |
19 36
|
syl5eq |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ∅ ) |
| 38 |
|
ioossicc |
⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) |
| 39 |
|
iccssre |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) |
| 40 |
39
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) |
| 41 |
|
ovolicc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵 − 𝐴 ) ) |
| 42 |
27 20
|
resubcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℝ ) |
| 43 |
41 42
|
eqeltrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ ) |
| 44 |
|
ovolsscl |
⊢ ( ( ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) |
| 45 |
38 40 43 44
|
mp3an2i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) |
| 46 |
3 45
|
eqeltrid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) |
| 47 |
|
mblvol |
⊢ ( { 𝐴 , 𝐵 } ∈ dom vol → ( vol ‘ { 𝐴 , 𝐵 } ) = ( vol* ‘ { 𝐴 , 𝐵 } ) ) |
| 48 |
15 47
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ { 𝐴 , 𝐵 } ) = ( vol* ‘ { 𝐴 , 𝐵 } ) ) |
| 49 |
48 13
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ { 𝐴 , 𝐵 } ) = 0 ) |
| 50 |
|
0re |
⊢ 0 ∈ ℝ |
| 51 |
49 50
|
eqeltrdi |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ { 𝐴 , 𝐵 } ) ∈ ℝ ) |
| 52 |
|
volun |
⊢ ( ( ( ( 𝐴 (,) 𝐵 ) ∈ dom vol ∧ { 𝐴 , 𝐵 } ∈ dom vol ∧ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ∅ ) ∧ ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ∧ ( vol ‘ { 𝐴 , 𝐵 } ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) ) = ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐴 , 𝐵 } ) ) ) |
| 53 |
8 15 37 46 51 52
|
syl32anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) ) = ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐴 , 𝐵 } ) ) ) |
| 54 |
|
rexr |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* ) |
| 55 |
|
rexr |
⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* ) |
| 56 |
|
id |
⊢ ( 𝐴 ≤ 𝐵 → 𝐴 ≤ 𝐵 ) |
| 57 |
|
prunioo |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) ) |
| 58 |
54 55 56 57
|
syl3an |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) ) |
| 59 |
58
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) ) = ( vol ‘ ( 𝐴 [,] 𝐵 ) ) ) |
| 60 |
49
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐴 , 𝐵 } ) ) = ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + 0 ) ) |
| 61 |
46
|
recnd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℂ ) |
| 62 |
61
|
addid1d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + 0 ) = ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ) |
| 63 |
60 62
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐴 , 𝐵 } ) ) = ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ) |
| 64 |
53 59 63
|
3eqtr3d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ) |
| 65 |
7 64 41
|
3eqtr3d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) ) |
| 66 |
3 65
|
eqtr3id |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) ) |