Metamath Proof Explorer


Theorem volicore

Description: The Lebesgue measure of a left-closed right-open interval is a real number. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Assertion volicore ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 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 ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )