Metamath Proof Explorer


Theorem voliccico

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

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

Proof

Step Hyp Ref Expression
1 voliccico.1
 |-  ( ph -> A e. RR )
2 voliccico.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 volicc
 |-  ( ( 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 simpr
 |-  ( ( ph /\ B < A ) -> B < A )
39 1 rexrd
 |-  ( ph -> A e. RR* )
40 2 rexrd
 |-  ( ph -> B e. RR* )
41 icc0
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) )
42 39 40 41 syl2anc
 |-  ( ph -> ( ( A [,] B ) = (/) <-> B < A ) )
43 42 adantr
 |-  ( ( ph /\ B < A ) -> ( ( A [,] B ) = (/) <-> B < A ) )
44 38 43 mpbird
 |-  ( ( ph /\ B < A ) -> ( A [,] B ) = (/) )
45 2 adantr
 |-  ( ( ph /\ B < A ) -> B e. RR )
46 1 adantr
 |-  ( ( ph /\ B < A ) -> A e. RR )
47 45 46 38 ltled
 |-  ( ( ph /\ B < A ) -> B <_ A )
48 46 rexrd
 |-  ( ( ph /\ B < A ) -> A e. RR* )
49 45 rexrd
 |-  ( ( ph /\ B < A ) -> B e. RR* )
50 ico0
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
51 48 49 50 syl2anc
 |-  ( ( ph /\ B < A ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
52 47 51 mpbird
 |-  ( ( ph /\ B < A ) -> ( A [,) B ) = (/) )
53 44 52 eqtr4d
 |-  ( ( ph /\ B < A ) -> ( A [,] B ) = ( A [,) B ) )
54 53 fveq2d
 |-  ( ( ph /\ B < A ) -> ( vol ` ( A [,] B ) ) = ( vol ` ( A [,) B ) ) )
55 32 37 54 syl2anc
 |-  ( ( ph /\ -. A <_ B ) -> ( vol ` ( A [,] B ) ) = ( vol ` ( A [,) B ) ) )
56 31 55 pm2.61dan
 |-  ( ph -> ( vol ` ( A [,] B ) ) = ( vol ` ( A [,) B ) ) )