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