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 ) )