Metamath Proof Explorer

Theorem volioore

Description: The measure of an open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion volioore 
|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )

Proof

Step Hyp Ref Expression
1 volioo 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
2 1 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
3 iftrue 
 |-  ( A <_ B -> if ( A <_ B , ( B - A ) , 0 ) = ( B - A ) )
4 3 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> if ( A <_ B , ( B - A ) , 0 ) = ( B - A ) )
5 2 4 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )
6 simpl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> ( A e. RR /\ B e. RR ) )
7 simpr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> -. A <_ B )
8 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
9 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
10 8 9 ltnled 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B < A <-> -. A <_ B ) )
11 10 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> ( B < A <-> -. A <_ B ) )
12 7 11 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> B < A )
13 vol0 
 |-  ( vol ` (/) ) = 0
14 13 a1i 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( vol ` (/) ) = 0 )
15 8 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> B e. RR )
16 9 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> A e. RR )
17 simpr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> B < A )
18 15 16 17 ltled 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> B <_ A )
19 9 rexrd 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR* )
20 8 rexrd 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR* )
21 ioo0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
22 19 20 21 syl2anc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
23 22 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
24 18 23 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( A (,) B ) = (/) )
25 24 fveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( vol ` ( A (,) B ) ) = ( vol ` (/) ) )
26 10 biimpa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> -. A <_ B )
27 26 iffalsed 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> if ( A <_ B , ( B - A ) , 0 ) = 0 )
28 14 25 27 3eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( vol ` ( A (,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )
29 6 12 28 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> ( vol ` ( A (,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )
30 5 29 pm2.61dan 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )