Metamath Proof Explorer

Theorem sublevolico

Description: The Lebesgue measure of a left-closed, right-open interval is greater than or equal to the difference of the two bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses sublevolico.a 
|- ( ph -> A e. RR )
sublevolico.b 
|- ( ph -> B e. RR )
Assertion sublevolico 
|- ( ph -> ( B - A ) <_ ( vol ` ( A [,) B ) ) )

Proof

Step Hyp Ref Expression
1 sublevolico.a 
 |-  ( ph -> A e. RR )
2 sublevolico.b 
 |-  ( ph -> B e. RR )
3 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
4 eqidd 
 |-  ( ph -> ( B - A ) = ( B - A ) )
5 3 4 eqled 
 |-  ( ph -> ( B - A ) <_ ( B - A ) )
6 5 adantr 
 |-  ( ( ph /\ A < B ) -> ( B - A ) <_ ( B - A ) )
7 volico 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
8 1 2 7 syl2anc 
 |-  ( ph -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
9 8 adantr 
 |-  ( ( ph /\ A < B ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
10 iftrue 
 |-  ( A < B -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
11 10 adantl 
 |-  ( ( ph /\ A < B ) -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
12 9 11 eqtr2d 
 |-  ( ( ph /\ A < B ) -> ( B - A ) = ( vol ` ( A [,) B ) ) )
13 6 12 breqtrd 
 |-  ( ( ph /\ A < B ) -> ( B - A ) <_ ( vol ` ( A [,) B ) ) )
14 simpr 
 |-  ( ( ph /\ -. A < B ) -> -. A < B )
15 2 1 lenltd 
 |-  ( ph -> ( B <_ A <-> -. A < B ) )
16 15 adantr 
 |-  ( ( ph /\ -. A < B ) -> ( B <_ A <-> -. A < B ) )
17 14 16 mpbird 
 |-  ( ( ph /\ -. A < B ) -> B <_ A )
18 2 adantr 
 |-  ( ( ph /\ -. A < B ) -> B e. RR )
19 1 adantr 
 |-  ( ( ph /\ -. A < B ) -> A e. RR )
20 18 19 suble0d 
 |-  ( ( ph /\ -. A < B ) -> ( ( B - A ) <_ 0 <-> B <_ A ) )
21 17 20 mpbird 
 |-  ( ( ph /\ -. A < B ) -> ( B - A ) <_ 0 )
22 8 adantr 
 |-  ( ( ph /\ -. A < B ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
23 iffalse 
 |-  ( -. A < B -> if ( A < B , ( B - A ) , 0 ) = 0 )
24 23 adantl 
 |-  ( ( ph /\ -. A < B ) -> if ( A < B , ( B - A ) , 0 ) = 0 )
25 22 24 eqtr2d 
 |-  ( ( ph /\ -. A < B ) -> 0 = ( vol ` ( A [,) B ) ) )
26 21 25 breqtrd 
 |-  ( ( ph /\ -. A < B ) -> ( B - A ) <_ ( vol ` ( A [,) B ) ) )
27 13 26 pm2.61dan 
 |-  ( ph -> ( B - A ) <_ ( vol ` ( A [,) B ) ) )