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