This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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