Metamath Proof Explorer

Theorem iccvolcl

Description: A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014)

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

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 rexr 
 |-  ( A e. RR -> A e. RR* )
5 rexr 
 |-  ( B e. RR -> B e. RR* )
6 icc0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) )
7 4 5 6 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A [,] B ) = (/) <-> B < A ) )
8 7 biimpar 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( A [,] B ) = (/) )
9 fveq2 
 |-  ( ( A [,] B ) = (/) -> ( vol* ` ( A [,] B ) ) = ( vol* ` (/) ) )
10 ovol0 
 |-  ( vol* ` (/) ) = 0
11 9 10 eqtrdi 
 |-  ( ( A [,] B ) = (/) -> ( vol* ` ( A [,] B ) ) = 0 )
12 0re 
 |-  0 e. RR
13 11 12 eqeltrdi 
 |-  ( ( A [,] B ) = (/) -> ( vol* ` ( A [,] B ) ) e. RR )
14 8 13 syl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( vol* ` ( A [,] B ) ) e. RR )
15 ovolicc 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) = ( B - A ) )
16 15 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) = ( B - A ) )
17 resubcl 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B - A ) e. RR )
18 17 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B - A ) e. RR )
19 18 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( B - A ) e. RR )
20 16 19 eqeltrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) e. RR )
21 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
22 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
23 14 20 21 22 ltlecasei 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol* ` ( A [,] B ) ) e. RR )
24 3 23 eqeltrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,] B ) ) e. RR )