Metamath Proof Explorer

Theorem volioc

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

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

Proof

Step Hyp Ref Expression
1 vol0 
 |-  ( vol ` (/) ) = 0
2 oveq2 
 |-  ( A = B -> ( A (,] A ) = ( A (,] B ) )
3 2 eqcomd 
 |-  ( A = B -> ( A (,] B ) = ( A (,] A ) )
4 leid 
 |-  ( A e. RR -> A <_ A )
5 rexr 
 |-  ( A e. RR -> A e. RR* )
6 ioc0 
 |-  ( ( A e. RR* /\ A e. RR* ) -> ( ( A (,] A ) = (/) <-> A <_ A ) )
7 5 5 6 syl2anc 
 |-  ( A e. RR -> ( ( A (,] A ) = (/) <-> A <_ A ) )
8 4 7 mpbird 
 |-  ( A e. RR -> ( A (,] A ) = (/) )
9 3 8 sylan9eqr 
 |-  ( ( A e. RR /\ A = B ) -> ( A (,] B ) = (/) )
10 9 fveq2d 
 |-  ( ( A e. RR /\ A = B ) -> ( vol ` ( A (,] B ) ) = ( vol ` (/) ) )
11 eqcom 
 |-  ( A = B <-> B = A )
12 11 biimpi 
 |-  ( A = B -> B = A )
13 12 adantl 
 |-  ( ( A e. RR /\ A = B ) -> B = A )
14 recn 
 |-  ( A e. RR -> A e. CC )
15 14 adantr 
 |-  ( ( A e. RR /\ A = B ) -> A e. CC )
16 13 15 eqeltrd 
 |-  ( ( A e. RR /\ A = B ) -> B e. CC )
17 16 13 subeq0bd 
 |-  ( ( A e. RR /\ A = B ) -> ( B - A ) = 0 )
18 1 10 17 3eqtr4a 
 |-  ( ( A e. RR /\ A = B ) -> ( vol ` ( A (,] B ) ) = ( B - A ) )
19 18 3ad2antl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ A = B ) -> ( vol ` ( A (,] B ) ) = ( B - A ) )
20 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ -. A = B ) -> A e. RR )
21 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ -. A = B ) -> B e. RR )
22 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ -. A = B ) -> A <_ B )
23 eqcom 
 |-  ( B = A <-> A = B )
24 23 biimpi 
 |-  ( B = A -> A = B )
25 24 necon3bi 
 |-  ( -. A = B -> B =/= A )
26 25 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ -. A = B ) -> B =/= A )
27 20 21 22 26 leneltd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ -. A = B ) -> A < B )
28 5 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. RR* )
29 rexr 
 |-  ( B e. RR -> B e. RR* )
30 29 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. RR* )
31 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A < B )
32 ioounsn 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
33 28 30 31 32 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
34 33 eqcomd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( A (,] B ) = ( ( A (,) B ) u. { B } ) )
35 34 fveq2d 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` ( A (,] B ) ) = ( vol ` ( ( A (,) B ) u. { B } ) ) )
36 ioombl 
 |-  ( A (,) B ) e. dom vol
37 36 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( A (,) B ) e. dom vol )
38 snmbl 
 |-  ( B e. RR -> { B } e. dom vol )
39 38 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> { B } e. dom vol )
40 ubioo 
 |-  -. B e. ( A (,) B )
41 disjsn 
 |-  ( ( ( A (,) B ) i^i { B } ) = (/) <-> -. B e. ( A (,) B ) )
42 40 41 mpbir 
 |-  ( ( A (,) B ) i^i { B } ) = (/)
43 42 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A (,) B ) i^i { B } ) = (/) )
44 ioovolcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) e. RR )
45 44 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` ( A (,) B ) ) e. RR )
46 volsn 
 |-  ( B e. RR -> ( vol ` { B } ) = 0 )
47 0red 
 |-  ( B e. RR -> 0 e. RR )
48 46 47 eqeltrd 
 |-  ( B e. RR -> ( vol ` { B } ) e. RR )
49 48 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` { B } ) e. RR )
50 volun 
 |-  ( ( ( ( A (,) B ) e. dom vol /\ { B } e. dom vol /\ ( ( A (,) B ) i^i { B } ) = (/) ) /\ ( ( vol ` ( A (,) B ) ) e. RR /\ ( vol ` { B } ) e. RR ) ) -> ( vol ` ( ( A (,) B ) u. { B } ) ) = ( ( vol ` ( A (,) B ) ) + ( vol ` { B } ) ) )
51 37 39 43 45 49 50 syl32anc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` ( ( A (,) B ) u. { B } ) ) = ( ( vol ` ( A (,) B ) ) + ( vol ` { B } ) ) )
52 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. RR )
53 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. RR )
54 52 53 31 ltled 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A <_ B )
55 volioo 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
56 52 53 54 55 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
57 46 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` { B } ) = 0 )
58 56 57 oveq12d 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( vol ` ( A (,) B ) ) + ( vol ` { B } ) ) = ( ( B - A ) + 0 ) )
59 53 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. CC )
60 14 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. CC )
61 59 60 subcld 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. CC )
62 61 addridd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( B - A ) + 0 ) = ( B - A ) )
63 58 62 eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( vol ` ( A (,) B ) ) + ( vol ` { B } ) ) = ( B - A ) )
64 35 51 63 3eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( vol ` ( A (,] B ) ) = ( B - A ) )
65 20 21 27 64 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ -. A = B ) -> ( vol ` ( A (,] B ) ) = ( B - A ) )
66 19 65 pm2.61dan 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,] B ) ) = ( B - A ) )