Theorem volicorecl

Description: The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	volicorecl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		volico	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
2		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
3		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
4	2 3	resubcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
5		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ∈ ℝ )
6	4 5	ifcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) ∈ ℝ )
7	1 6	eqeltrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )