Metamath Proof Explorer

Theorem volicorecl

Description: The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion volicorecl A B vol A B


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