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	|- ( ph -> A e. RR )
	volicon0.2	|- ( ph -> B e. RR )
	volicon0.3	|- ( ph -> A < B )
Assertion	volicon0	|- ( ph -> ( vol ` ( A [,) B ) ) = ( B - A ) )

Proof

Step	Hyp	Ref	Expression
1		volicon0.1	|- ( ph -> A e. RR )
2		volicon0.2	|- ( ph -> B e. RR )
3		volicon0.3	|- ( ph -> A < B )
4		volico	|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
5	1 2 4	syl2anc	|- ( ph -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
6	3	iftrued	|- ( ph -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
7	5 6	eqtrd	|- ( ph -> ( vol ` ( A [,) B ) ) = ( B - A ) )