volicc

Description: The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021)

		Ref	Expression
	Assertion	volicc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ([A, B]) = B - A$

Step	Hyp	Ref	Expression
1		iccmbl	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \in dom vol$
2		mblvol	$⊢ [A, B] \in dom vol \to vol ([A, B]) = {vol}^{*} ([A, B])$
3	1 2	syl	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B]) = {vol}^{*} ([A, B])$
4	3	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ([A, B]) = {vol}^{*} ([A, B])$
5		ovolicc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ([A, B]) = B - A$
6	4 5	eqtrd	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ([A, B]) = B - A$

Metamath Proof Explorer