Theorem volicon0

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

	Ref	Expression
Hypotheses	volicon0.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	volicon0.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	volicon0.3	⊢ ( 𝜑 → 𝐴 < 𝐵 )
Assertion	volicon0	⊢ ( 𝜑 → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		volicon0.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		volicon0.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		volicon0.3	⊢ ( 𝜑 → 𝐴 < 𝐵 )
4		volico	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
5	1 2 4	syl2anc	⊢ ( 𝜑 → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
6	3	iftrued	⊢ ( 𝜑 → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
7	5 6	eqtrd	⊢ ( 𝜑 → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )