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	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to vol\left(\left[A,B\right)\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		volico	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to vol\left(\left[A,B\right)\right)=if\left(A<B,B-A,0\right)$$
2		simpr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℝ$$
3		simpl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\in ℝ$$
4	2 3	resubcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B-A\in ℝ$$
5		0red	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to 0\in ℝ$$
6	4 5	ifcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to if\left(A<B,B-A,0\right)\in ℝ$$
7	1 6	eqeltrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to vol\left(\left[A,B\right)\right)\in ℝ$$