Metamath Proof Explorer

Theorem ovolioo

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

Ref Expression
Assertion ovolioo 
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A (,) B ) ) = ( B - A ) )

Proof

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