Metamath Proof Explorer

Theorem volico

Description: The measure of left-closed, right-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion volico 
|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )

Proof

Step Hyp Ref Expression
1 rexr 
 |-  ( A e. RR -> A e. RR* )
2 1 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. RR* )
3 rexr 
 |-  ( B e. RR -> B e. RR* )
4 3 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. RR* )
5 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A < B )
6 snunioo1 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { A } ) = ( A [,) B ) )
7 2 4 5 6 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A (,) B ) u. { A } ) = ( A [,) B ) )
8 7 eqcomd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( A [,) B ) = ( ( A (,) B ) u. { A } ) )
9 8 fveq2d 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` ( A [,) B ) ) = ( vol ` ( ( A (,) B ) u. { A } ) ) )
10 ioombl 
 |-  ( A (,) B ) e. dom vol
11 10 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( A (,) B ) e. dom vol )
12 snmbl 
 |-  ( A e. RR -> { A } e. dom vol )
13 12 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> { A } e. dom vol )
14 lbioo 
 |-  -. A e. ( A (,) B )
15 disjsn 
 |-  ( ( ( A (,) B ) i^i { A } ) = (/) <-> -. A e. ( A (,) B ) )
16 14 15 mpbir 
 |-  ( ( A (,) B ) i^i { A } ) = (/)
17 16 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A (,) B ) i^i { A } ) = (/) )
18 ioovolcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) e. RR )
19 18 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` ( A (,) B ) ) e. RR )
20 volsn 
 |-  ( A e. RR -> ( vol ` { A } ) = 0 )
21 0red 
 |-  ( A e. RR -> 0 e. RR )
22 20 21 eqeltrd 
 |-  ( A e. RR -> ( vol ` { A } ) e. RR )
23 22 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` { A } ) e. RR )
24 volun 
 |-  ( ( ( ( A (,) B ) e. dom vol /\ { A } e. dom vol /\ ( ( A (,) B ) i^i { A } ) = (/) ) /\ ( ( vol ` ( A (,) B ) ) e. RR /\ ( vol ` { A } ) e. RR ) ) -> ( vol ` ( ( A (,) B ) u. { A } ) ) = ( ( vol ` ( A (,) B ) ) + ( vol ` { A } ) ) )
25 11 13 17 19 23 24 syl32anc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` ( ( A (,) B ) u. { A } ) ) = ( ( vol ` ( A (,) B ) ) + ( vol ` { A } ) ) )
26 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. RR )
27 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. RR )
28 26 27 5 ltled 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A <_ B )
29 volioo 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
30 26 27 28 29 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
31 20 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` { A } ) = 0 )
32 30 31 oveq12d 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( vol ` ( A (,) B ) ) + ( vol ` { A } ) ) = ( ( B - A ) + 0 ) )
33 27 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. CC )
34 recn 
 |-  ( A e. RR -> A e. CC )
35 34 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. CC )
36 33 35 subcld 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. CC )
37 36 addid1d 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( B - A ) + 0 ) = ( B - A ) )
38 32 37 eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( vol ` ( A (,) B ) ) + ( vol ` { A } ) ) = ( B - A ) )
39 9 25 38 3eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` ( A [,) B ) ) = ( B - A ) )
40 39 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> ( vol ` ( A [,) B ) ) = ( B - A ) )
41 iftrue 
 |-  ( A < B -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
42 41 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
43 40 42 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
44 simpl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A < B ) -> ( A e. RR /\ B e. RR ) )
45 simpr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A < B ) -> -. A < B )
46 44 simprd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A < B ) -> B e. RR )
47 44 simpld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A < B ) -> A e. RR )
48 46 47 lenltd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A < B ) -> ( B <_ A <-> -. A < B ) )
49 45 48 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A < B ) -> B <_ A )
50 simpr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B <_ A ) -> B <_ A )
51 1 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B <_ A ) -> A e. RR* )
52 3 ad2antlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B <_ A ) -> B e. RR* )
53 ico0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
54 51 52 53 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B <_ A ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
55 50 54 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B <_ A ) -> ( A [,) B ) = (/) )
56 55 fveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B <_ A ) -> ( vol ` ( A [,) B ) ) = ( vol ` (/) ) )
57 vol0 
 |-  ( vol ` (/) ) = 0
58 57 a1i 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B <_ A ) -> ( vol ` (/) ) = 0 )
59 56 58 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B <_ A ) -> ( vol ` ( A [,) B ) ) = 0 )
60 44 49 59 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A < B ) -> ( vol ` ( A [,) B ) ) = 0 )
61 iffalse 
 |-  ( -. A < B -> if ( A < B , ( B - A ) , 0 ) = 0 )
62 61 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A < B ) -> if ( A < B , ( B - A ) , 0 ) = 0 )
63 60 62 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A < B ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
64 43 63 pm2.61dan 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )