Metamath Proof Explorer

Theorem iocinif

Description: Relate intersection of two open-below, closed-above intervals with the same upper bound with a conditional construct. (Contributed by Thierry Arnoux, 7-Aug-2017)

Ref Expression
Assertion iocinif 
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A (,] C ) i^i ( B (,] C ) ) = if ( A < B , ( B (,] C ) , ( A (,] C ) ) )

Proof

Step Hyp Ref Expression
1 exmid 
 |-  ( A < B \/ -. A < B )
2 xrltle 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> A <_ B ) )
3 2 imp 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ A < B ) -> A <_ B )
4 3 3adantl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) -> A <_ B )
5 iocinioc2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( ( A (,] C ) i^i ( B (,] C ) ) = ( B (,] C ) )
6 4 5 syldan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < B ) -> ( ( A (,] C ) i^i ( B (,] C ) ) = ( B (,] C ) )
7 6 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A < B -> ( ( A (,] C ) i^i ( B (,] C ) ) = ( B (,] C ) ) )
8 7 ancld 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A < B -> ( A < B /\ ( ( A (,] C ) i^i ( B (,] C ) ) = ( B (,] C ) ) ) )
9 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ -. A < B ) -> B e. RR* )
10 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ -. A < B ) -> A e. RR* )
11 simpr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ -. A < B ) -> -. A < B )
12 xrlenlt 
 |-  ( ( B e. RR* /\ A e. RR* ) -> ( B <_ A <-> -. A < B ) )
13 12 biimpar 
 |-  ( ( ( B e. RR* /\ A e. RR* ) /\ -. A < B ) -> B <_ A )
14 9 10 11 13 syl21anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ -. A < B ) -> B <_ A )
15 3ancoma 
 |-  ( ( B e. RR* /\ A e. RR* /\ C e. RR* ) <-> ( A e. RR* /\ B e. RR* /\ C e. RR* ) )
16 incom 
 |-  ( ( B (,] C ) i^i ( A (,] C ) ) = ( ( A (,] C ) i^i ( B (,] C ) )
17 iocinioc2 
 |-  ( ( ( B e. RR* /\ A e. RR* /\ C e. RR* ) /\ B <_ A ) -> ( ( B (,] C ) i^i ( A (,] C ) ) = ( A (,] C ) )
18 16 17 eqtr3id 
 |-  ( ( ( B e. RR* /\ A e. RR* /\ C e. RR* ) /\ B <_ A ) -> ( ( A (,] C ) i^i ( B (,] C ) ) = ( A (,] C ) )
19 15 18 sylanbr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ B <_ A ) -> ( ( A (,] C ) i^i ( B (,] C ) ) = ( A (,] C ) )
20 14 19 syldan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ -. A < B ) -> ( ( A (,] C ) i^i ( B (,] C ) ) = ( A (,] C ) )
21 20 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( -. A < B -> ( ( A (,] C ) i^i ( B (,] C ) ) = ( A (,] C ) ) )
22 21 ancld 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( -. A < B -> ( -. A < B /\ ( ( A (,] C ) i^i ( B (,] C ) ) = ( A (,] C ) ) ) )
23 8 22 orim12d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B \/ -. A < B ) -> ( ( A < B /\ ( ( A (,] C ) i^i ( B (,] C ) ) = ( B (,] C ) ) \/ ( -. A < B /\ ( ( A (,] C ) i^i ( B (,] C ) ) = ( A (,] C ) ) ) ) )
24 1 23 mpi 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ ( ( A (,] C ) i^i ( B (,] C ) ) = ( B (,] C ) ) \/ ( -. A < B /\ ( ( A (,] C ) i^i ( B (,] C ) ) = ( A (,] C ) ) ) )
25 eqif 
 |-  ( ( ( A (,] C ) i^i ( B (,] C ) ) = if ( A < B , ( B (,] C ) , ( A (,] C ) ) <-> ( ( A < B /\ ( ( A (,] C ) i^i ( B (,] C ) ) = ( B (,] C ) ) \/ ( -. A < B /\ ( ( A (,] C ) i^i ( B (,] C ) ) = ( A (,] C ) ) ) )
26 24 25 sylibr 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A (,] C ) i^i ( B (,] C ) ) = if ( A < B , ( B (,] C ) , ( A (,] C ) ) )