This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ioovolcl

Description: An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 ioombl 
 |-  ( A (,) B ) e. dom vol
2 mblvol 
 |-  ( ( A (,) B ) e. dom vol -> ( vol ` ( A (,) B ) ) = ( vol* ` ( A (,) B ) ) )
3 1 2 mp1i 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) = ( vol* ` ( A (,) B ) ) )
4 ltle 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B < A -> B <_ A ) )
5 4 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B < A -> B <_ A ) )
6 5 imdistani 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( ( A e. RR /\ B e. RR ) /\ B <_ A ) )
7 rexr 
 |-  ( A e. RR -> A e. RR* )
8 rexr 
 |-  ( B e. RR -> B e. RR* )
9 ioo0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
10 7 8 9 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
11 10 biimpar 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B <_ A ) -> ( A (,) B ) = (/) )
12 fveq2 
 |-  ( ( A (,) B ) = (/) -> ( vol* ` ( A (,) B ) ) = ( vol* ` (/) ) )
13 ovol0 
 |-  ( vol* ` (/) ) = 0
14 12 13 eqtrdi 
 |-  ( ( A (,) B ) = (/) -> ( vol* ` ( A (,) B ) ) = 0 )
15 0re 
 |-  0 e. RR
16 14 15 eqeltrdi 
 |-  ( ( A (,) B ) = (/) -> ( vol* ` ( A (,) B ) ) e. RR )
17 6 11 16 3syl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( vol* ` ( A (,) B ) ) e. RR )
18 ovolioo 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A (,) B ) ) = ( B - A ) )
19 18 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( vol* ` ( A (,) B ) ) = ( B - A ) )
20 resubcl 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B - A ) e. RR )
21 20 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B - A ) e. RR )
22 21 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( B - A ) e. RR )
23 19 22 eqeltrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( vol* ` ( A (,) B ) ) e. RR )
24 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
25 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
26 17 23 24 25 ltlecasei 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol* ` ( A (,) B ) ) e. RR )
27 3 26 eqeltrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) e. RR )