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	$$⊢\phi \to A\in ℝ$$
	volicon0.2	$$⊢\phi \to B\in ℝ$$
	volicon0.3	$$⊢\phi \to A<B$$
Assertion	volicon0	$$⊢\phi \to vol\left(\left[A,B\right)\right)=B-A$$

Proof

Step	Hyp	Ref	Expression
1		volicon0.1	$$⊢\phi \to A\in ℝ$$
2		volicon0.2	$$⊢\phi \to B\in ℝ$$
3		volicon0.3	$$⊢\phi \to A<B$$
4		volico	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to vol\left(\left[A,B\right)\right)=if\left(A<B,B-A,0\right)$$
5	1 2 4	syl2anc	$$⊢\phi \to vol\left(\left[A,B\right)\right)=if\left(A<B,B-A,0\right)$$
6	3	iftrued	$$⊢\phi \to if\left(A<B,B-A,0\right)=B-A$$
7	5 6	eqtrd	$$⊢\phi \to vol\left(\left[A,B\right)\right)=B-A$$