iccvolcl

Description: A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014)

		Ref	Expression
	Assertion	iccvolcl	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B]) \in ℝ$

Proof

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		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
5		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
6		icc0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$
7	4 5 6	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to ([A, B] = \emptyset \leftrightarrow B < A)$
8	7	biimpar	$⊢ ((A \in ℝ \land B \in ℝ) \land B < A) \to [A, B] = \emptyset$
9		fveq2	$⊢ [A, B] = \emptyset \to {vol}^{} ([A, B]) = {vol}^{} (\emptyset)$
10		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
11	9 10	eqtrdi	$⊢ [A, B] = \emptyset \to {vol}^{*} ([A, B]) = 0$
12		0re	$⊢ 0 \in ℝ$
13	11 12	eqeltrdi	$⊢ [A, B] = \emptyset \to {vol}^{*} ([A, B]) \in ℝ$
14	8 13	syl	$⊢ ((A \in ℝ \land B \in ℝ) \land B < A) \to {vol}^{*} ([A, B]) \in ℝ$
15		ovolicc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ([A, B]) = B - A$
16	15	3expa	$⊢ ((A \in ℝ \land B \in ℝ) \land A \leq B) \to {vol}^{*} ([A, B]) = B - A$
17		resubcl	$⊢ (B \in ℝ \land A \in ℝ) \to B - A \in ℝ$
18	17	ancoms	$⊢ (A \in ℝ \land B \in ℝ) \to B - A \in ℝ$
19	18	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land A \leq B) \to B - A \in ℝ$
20	16 19	eqeltrd	$⊢ ((A \in ℝ \land B \in ℝ) \land A \leq B) \to {vol}^{*} ([A, B]) \in ℝ$
21		simpr	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ$
22		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
23	14 20 21 22	ltlecasei	$⊢ (A \in ℝ \land B \in ℝ) \to {vol}^{*} ([A, B]) \in ℝ$
24	3 23	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B]) \in ℝ$

Metamath Proof Explorer

Theorem iccvolcl

Proof