Metamath Proof Explorer


Theorem volicore

Description: The Lebesgue measure of a left-closed right-open interval is a real number. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Assertion volicore
|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) e. RR )

Proof

Step Hyp Ref Expression
1 volico
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
2 simpr
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
3 simpl
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
4 2 3 resubcld
 |-  ( ( A e. RR /\ B e. RR ) -> ( B - A ) e. RR )
5 0red
 |-  ( ( A e. RR /\ B e. RR ) -> 0 e. RR )
6 4 5 ifcld
 |-  ( ( A e. RR /\ B e. RR ) -> if ( A < B , ( B - A ) , 0 ) e. RR )
7 1 6 eqeltrd
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) e. RR )