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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ∈ ℝ )
2	1	rexrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ∈ ℝ* )
3		pnfxr	⊢ +∞ ∈ ℝ*
4	3	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → +∞ ∈ ℝ* )
5		volicore	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )
6	5	rexrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ℝ* )
7		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
8		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
9	8	rexrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ* )
10		icombl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
11	7 9 10	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
12		volge0	⊢ ( ( 𝐴 [,) 𝐵 ) ∈ dom vol → 0 ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
13	11 12	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
14	5	ltpnfd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) < +∞ )
15	2 4 6 13 14	elicod	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ( 0 [,) +∞ ) )