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

Proof

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