Metamath Proof Explorer


Theorem voliooico

Description: An open interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses voliooico.1
|- ( ph -> A e. RR )
voliooico.2
|- ( ph -> B e. RR )
Assertion voliooico
|- ( ph -> ( vol ` ( A (,) B ) ) = ( vol ` ( A [,) B ) ) )

Proof

Step Hyp Ref Expression
1 voliooico.1
 |-  ( ph -> A e. RR )
2 voliooico.2
 |-  ( ph -> B e. RR )
3 iftrue
 |-  ( A < B -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
4 3 adantl
 |-  ( ( ( ph /\ A <_ B ) /\ A < B ) -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
5 2 recnd
 |-  ( ph -> B e. CC )
6 5 subidd
 |-  ( ph -> ( B - B ) = 0 )
7 6 eqcomd
 |-  ( ph -> 0 = ( B - B ) )
8 7 ad2antrr
 |-  ( ( ( ph /\ A <_ B ) /\ -. A < B ) -> 0 = ( B - B ) )
9 iffalse
 |-  ( -. A < B -> if ( A < B , ( B - A ) , 0 ) = 0 )
10 9 adantl
 |-  ( ( ( ph /\ A <_ B ) /\ -. A < B ) -> if ( A < B , ( B - A ) , 0 ) = 0 )
11 simpll
 |-  ( ( ( ph /\ A <_ B ) /\ -. A < B ) -> ph )
12 11 1 syl
 |-  ( ( ( ph /\ A <_ B ) /\ -. A < B ) -> A e. RR )
13 11 2 syl
 |-  ( ( ( ph /\ A <_ B ) /\ -. A < B ) -> B e. RR )
14 simpr
 |-  ( ( ph /\ A <_ B ) -> A <_ B )
15 14 adantr
 |-  ( ( ( ph /\ A <_ B ) /\ -. A < B ) -> A <_ B )
16 simpr
 |-  ( ( ( ph /\ A <_ B ) /\ -. A < B ) -> -. A < B )
17 12 13 15 16 lenlteq
 |-  ( ( ( ph /\ A <_ B ) /\ -. A < B ) -> A = B )
18 oveq2
 |-  ( A = B -> ( B - A ) = ( B - B ) )
19 18 adantl
 |-  ( ( ph /\ A = B ) -> ( B - A ) = ( B - B ) )
20 11 17 19 syl2anc
 |-  ( ( ( ph /\ A <_ B ) /\ -. A < B ) -> ( B - A ) = ( B - B ) )
21 8 10 20 3eqtr4d
 |-  ( ( ( ph /\ A <_ B ) /\ -. A < B ) -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
22 4 21 pm2.61dan
 |-  ( ( ph /\ A <_ B ) -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
23 22 eqcomd
 |-  ( ( ph /\ A <_ B ) -> ( B - A ) = if ( A < B , ( B - A ) , 0 ) )
24 1 adantr
 |-  ( ( ph /\ A <_ B ) -> A e. RR )
25 2 adantr
 |-  ( ( ph /\ A <_ B ) -> B e. RR )
26 volioo
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
27 24 25 14 26 syl3anc
 |-  ( ( ph /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
28 volico
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
29 1 2 28 syl2anc
 |-  ( ph -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
30 29 adantr
 |-  ( ( ph /\ A <_ B ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
31 23 27 30 3eqtr4d
 |-  ( ( ph /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( vol ` ( A [,) B ) ) )
32 simpl
 |-  ( ( ph /\ -. A <_ B ) -> ph )
33 simpr
 |-  ( ( ph /\ -. A <_ B ) -> -. A <_ B )
34 32 2 syl
 |-  ( ( ph /\ -. A <_ B ) -> B e. RR )
35 32 1 syl
 |-  ( ( ph /\ -. A <_ B ) -> A e. RR )
36 34 35 ltnled
 |-  ( ( ph /\ -. A <_ B ) -> ( B < A <-> -. A <_ B ) )
37 33 36 mpbird
 |-  ( ( ph /\ -. A <_ B ) -> B < A )
38 2 adantr
 |-  ( ( ph /\ B < A ) -> B e. RR )
39 1 adantr
 |-  ( ( ph /\ B < A ) -> A e. RR )
40 simpr
 |-  ( ( ph /\ B < A ) -> B < A )
41 38 39 40 ltled
 |-  ( ( ph /\ B < A ) -> B <_ A )
42 39 rexrd
 |-  ( ( ph /\ B < A ) -> A e. RR* )
43 38 rexrd
 |-  ( ( ph /\ B < A ) -> B e. RR* )
44 ioo0
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
45 42 43 44 syl2anc
 |-  ( ( ph /\ B < A ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
46 41 45 mpbird
 |-  ( ( ph /\ B < A ) -> ( A (,) B ) = (/) )
47 ico0
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
48 42 43 47 syl2anc
 |-  ( ( ph /\ B < A ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
49 41 48 mpbird
 |-  ( ( ph /\ B < A ) -> ( A [,) B ) = (/) )
50 46 49 eqtr4d
 |-  ( ( ph /\ B < A ) -> ( A (,) B ) = ( A [,) B ) )
51 50 fveq2d
 |-  ( ( ph /\ B < A ) -> ( vol ` ( A (,) B ) ) = ( vol ` ( A [,) B ) ) )
52 32 37 51 syl2anc
 |-  ( ( ph /\ -. A <_ B ) -> ( vol ` ( A (,) B ) ) = ( vol ` ( A [,) B ) ) )
53 31 52 pm2.61dan
 |-  ( ph -> ( vol ` ( A (,) B ) ) = ( vol ` ( A [,) B ) ) )