Metamath Proof Explorer

Theorem difico

Description: The difference between two closed-below, open-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 13-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 icodisj 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A [,) B ) i^i ( B [,) C ) ) = (/) )
2 undif4 
 |-  ( ( ( A [,) B ) i^i ( B [,) C ) ) = (/) -> ( ( A [,) B ) u. ( ( B [,) C ) \ ( B [,) C ) ) ) = ( ( ( A [,) B ) u. ( B [,) C ) ) \ ( B [,) C ) ) )
3 1 2 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A [,) B ) u. ( ( B [,) C ) \ ( B [,) C ) ) ) = ( ( ( A [,) B ) u. ( B [,) C ) ) \ ( B [,) C ) ) )
4 3 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ B /\ B <_ C ) ) -> ( ( A [,) B ) u. ( ( B [,) C ) \ ( B [,) C ) ) ) = ( ( ( A [,) B ) u. ( B [,) C ) ) \ ( B [,) C ) ) )
5 difid 
 |-  ( ( B [,) C ) \ ( B [,) C ) ) = (/)
6 5 uneq2i 
 |-  ( ( A [,) B ) u. ( ( B [,) C ) \ ( B [,) C ) ) ) = ( ( A [,) B ) u. (/) )
7 un0 
 |-  ( ( A [,) B ) u. (/) ) = ( A [,) B )
8 6 7 eqtri 
 |-  ( ( A [,) B ) u. ( ( B [,) C ) \ ( B [,) C ) ) ) = ( A [,) B )
9 8 a1i 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ B /\ B <_ C ) ) -> ( ( A [,) B ) u. ( ( B [,) C ) \ ( B [,) C ) ) ) = ( A [,) B ) )
10 icoun 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ B /\ B <_ C ) ) -> ( ( A [,) B ) u. ( B [,) C ) ) = ( A [,) C ) )
11 10 difeq1d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ B /\ B <_ C ) ) -> ( ( ( A [,) B ) u. ( B [,) C ) ) \ ( B [,) C ) ) = ( ( A [,) C ) \ ( B [,) C ) ) )
12 4 9 11 3eqtr3rd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ B /\ B <_ C ) ) -> ( ( A [,) C ) \ ( B [,) C ) ) = ( A [,) B ) )