Metamath Proof Explorer

Theorem volicorege0

Description: The Lebesgue measure of a left-closed right-open interval with real bounds, is a nonnegative real number. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Assertion	volicorege0	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) \in [0, +∞)$

Proof

Step	Hyp	Ref	Expression
1		0red	$⊢ (A \in ℝ \land B \in ℝ) \to 0 \in ℝ$
2	1	rexrd	$⊢ (A \in ℝ \land B \in ℝ) \to 0 \in ℝ^{*}$
3		pnfxr	$⊢ +∞ \in ℝ^{*}$
4	3	a1i	$⊢ (A \in ℝ \land B \in ℝ) \to +∞ \in ℝ^{*}$
5		volicore	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) \in ℝ$
6	5	rexrd	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) \in ℝ^{*}$
7		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
8		simpr	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ$
9	8	rexrd	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ^{*}$
10		icombl	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to [A, B) \in dom vol$
11	7 9 10	syl2anc	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B) \in dom vol$
12		volge0	$⊢ [A, B) \in dom vol \to 0 \leq vol ([A, B))$
13	11 12	syl	$⊢ (A \in ℝ \land B \in ℝ) \to 0 \leq vol ([A, B))$
14	5	ltpnfd	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) < +∞$
15	2 4 6 13 14	elicod	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) \in [0, +∞)$