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 B vol A B

Proof

Step Hyp Ref Expression
1 volico A B vol A B = if A < B B A 0
2 simpr A B B
3 simpl A B A
4 2 3 resubcld A B B A
5 0red A B 0
6 4 5 ifcld A B if A < B B A 0
7 1 6 eqeltrd A B vol A B