Metamath Proof Explorer

Theorem difioo

Description: The difference between two open intervals sharing the same lower bound. (Contributed by Thierry Arnoux, 26-Sep-2017)

Ref Expression
Assertion difioo 
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) -> ( ( A (,) C ) \ ( A (,) B ) ) = ( B [,) C ) )

Proof

Step Hyp Ref Expression
1 incom 
 |-  ( ( A (,) B ) i^i ( B [,) C ) ) = ( ( B [,) C ) i^i ( A (,) B ) )
2 joiniooico 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B <_ C ) ) -> ( ( ( A (,) B ) i^i ( B [,) C ) ) = (/) /\ ( ( A (,) B ) u. ( B [,) C ) ) = ( A (,) C ) ) )
3 2 anassrs 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> ( ( ( A (,) B ) i^i ( B [,) C ) ) = (/) /\ ( ( A (,) B ) u. ( B [,) C ) ) = ( A (,) C ) ) )
4 3 simpld 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> ( ( A (,) B ) i^i ( B [,) C ) ) = (/) )
5 1 4 syl5eqr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> ( ( B [,) C ) i^i ( A (,) B ) ) = (/) )
6 3 simprd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> ( ( A (,) B ) u. ( B [,) C ) ) = ( A (,) C ) )
7 uncom 
 |-  ( ( B [,) C ) u. ( A (,) B ) ) = ( ( A (,) B ) u. ( B [,) C ) )
8 7 a1i 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> ( ( B [,) C ) u. ( A (,) B ) ) = ( ( A (,) B ) u. ( B [,) C ) ) )
9 simpll1 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> A e. RR* )
10 simpl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) -> C e. RR* )
11 10 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> C e. RR* )
12 9 xrleidd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> A <_ A )
13 simpr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> B <_ C )
14 ioossioo 
 |-  ( ( ( A e. RR* /\ C e. RR* ) /\ ( A <_ A /\ B <_ C ) ) -> ( A (,) B ) C_ ( A (,) C ) )
15 9 11 12 13 14 syl22anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> ( A (,) B ) C_ ( A (,) C ) )
16 ssequn2 
 |-  ( ( A (,) B ) C_ ( A (,) C ) <-> ( ( A (,) C ) u. ( A (,) B ) ) = ( A (,) C ) )
17 15 16 sylib 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> ( ( A (,) C ) u. ( A (,) B ) ) = ( A (,) C ) )
18 6 8 17 3eqtr4d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> ( ( B [,) C ) u. ( A (,) B ) ) = ( ( A (,) C ) u. ( A (,) B ) ) )
19 difeq 
 |-  ( ( ( A (,) C ) \ ( A (,) B ) ) = ( B [,) C ) <-> ( ( ( B [,) C ) i^i ( A (,) B ) ) = (/) /\ ( ( B [,) C ) u. ( A (,) B ) ) = ( ( A (,) C ) u. ( A (,) B ) ) ) )
20 5 18 19 sylanbrc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ B <_ C ) -> ( ( A (,) C ) \ ( A (,) B ) ) = ( B [,) C ) )
21 simpll1 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ C < B ) -> A e. RR* )
22 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) -> B e. RR* )
23 22 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ C < B ) -> B e. RR* )
24 21 xrleidd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ C < B ) -> A <_ A )
25 10 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ C < B ) -> C e. RR* )
26 simpr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ C < B ) -> C < B )
27 25 23 26 xrltled 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ C < B ) -> C <_ B )
28 ioossioo 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ A /\ C <_ B ) ) -> ( A (,) C ) C_ ( A (,) B ) )
29 21 23 24 27 28 syl22anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ C < B ) -> ( A (,) C ) C_ ( A (,) B ) )
30 ssdif0 
 |-  ( ( A (,) C ) C_ ( A (,) B ) <-> ( ( A (,) C ) \ ( A (,) B ) ) = (/) )
31 29 30 sylib 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ C < B ) -> ( ( A (,) C ) \ ( A (,) B ) ) = (/) )
32 ico0 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( ( B [,) C ) = (/) <-> C <_ B ) )
33 32 biimpar 
 |-  ( ( ( B e. RR* /\ C e. RR* ) /\ C <_ B ) -> ( B [,) C ) = (/) )
34 23 25 27 33 syl21anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ C < B ) -> ( B [,) C ) = (/) )
35 31 34 eqtr4d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) /\ C < B ) -> ( ( A (,) C ) \ ( A (,) B ) ) = ( B [,) C ) )
36 xrlelttric 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B <_ C \/ C < B ) )
37 22 10 36 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) -> ( B <_ C \/ C < B ) )
38 20 35 37 mpjaodan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) -> ( ( A (,) C ) \ ( A (,) B ) ) = ( B [,) C ) )