Metamath Proof Explorer

Theorem volico2

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

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

Proof

Step Hyp Ref Expression
1 iftrue 
 |-  ( A < B -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
2 1 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
3 volico 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
4 3 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
5 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> A e. RR )
6 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> B e. RR )
7 simpr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> A < B )
8 5 6 7 ltled 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> A <_ B )
9 8 iftrued 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> if ( A <_ B , ( B - A ) , 0 ) = ( B - A ) )
10 2 4 9 3eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> ( vol ` ( A [,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )
11 10 adantlr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ A < B ) -> ( vol ` ( A [,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )
12 simpll 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ -. A < B ) -> ( A e. RR /\ B e. RR ) )
13 12 simpld 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ -. A < B ) -> A e. RR )
14 12 simprd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ -. A < B ) -> B e. RR )
15 simplr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ -. A < B ) -> A <_ B )
16 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ -. A < B ) -> -. A < B )
17 13 14 15 16 lenlteq 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ -. A < B ) -> A = B )
18 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> B e. RR )
19 simpr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> A = B )
20 19 eqcomd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> B = A )
21 18 20 eqled 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> B <_ A )
22 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> A e. RR )
23 18 22 lenltd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> ( B <_ A <-> -. A < B ) )
24 21 23 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> -. A < B )
25 24 iffalsed 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> if ( A < B , ( B - A ) , 0 ) = 0 )
26 recn 
 |-  ( A e. RR -> A e. CC )
27 26 subidd 
 |-  ( A e. RR -> ( A - A ) = 0 )
28 27 eqcomd 
 |-  ( A e. RR -> 0 = ( A - A ) )
29 28 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> 0 = ( A - A ) )
30 oveq1 
 |-  ( A = B -> ( A - A ) = ( B - A ) )
31 30 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> ( A - A ) = ( B - A ) )
32 25 29 31 3eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> if ( A < B , ( B - A ) , 0 ) = ( B - A ) )
33 3 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
34 22 19 eqled 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> A <_ B )
35 34 iftrued 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> if ( A <_ B , ( B - A ) , 0 ) = ( B - A ) )
36 32 33 35 3eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = B ) -> ( vol ` ( A [,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )
37 12 17 36 syl2anc 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ -. A < B ) -> ( vol ` ( A [,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )
38 11 37 pm2.61dan 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( vol ` ( A [,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )
39 8 stoic1a 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> -. A < B )
40 39 iffalsed 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> if ( A < B , ( B - A ) , 0 ) = 0 )
41 3 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
42 iffalse 
 |-  ( -. A <_ B -> if ( A <_ B , ( B - A ) , 0 ) = 0 )
43 42 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> if ( A <_ B , ( B - A ) , 0 ) = 0 )
44 40 41 43 3eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> ( vol ` ( A [,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )
45 38 44 pm2.61dan 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )