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