Metamath Proof Explorer

Theorem ovolioo

Description: The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014)

Ref Expression
Assertion ovolioo ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )

Proof

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 syl5eqr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )