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

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 ℝ$

Metamath Proof Explorer