Metamath Proof Explorer

Theorem volicc

Description: The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion volicc 
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A [,] B ) ) = ( B - A ) )

Proof

Step Hyp Ref Expression
1 iccmbl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. dom vol )
2 mblvol 
 |-  ( ( A [,] B ) e. dom vol -> ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) ) )
3 1 2 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) ) )
4 3 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) ) )
5 ovolicc 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) = ( B - A ) )
6 4 5 eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A [,] B ) ) = ( B - A ) )