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 * B * C * A C B C = if A < B B C A C

Proof

Step Hyp Ref Expression
1 exmid A < B ¬ A < B
2 xrltle A * B * A < B A B
3 2 imp A * B * A < B A B
4 3 3adantl3 A * B * C * A < B A B
5 iocinioc2 A * B * C * A B A C B C = B C
6 4 5 syldan A * B * C * A < B A C B C = B C
7 6 ex A * B * C * A < B A C B C = B C
8 7 ancld A * B * C * A < B A < B A C B C = B C
9 simpl2 A * B * C * ¬ A < B B *
10 simpl1 A * B * C * ¬ A < B A *
11 simpr A * B * C * ¬ A < B ¬ A < B
12 xrlenlt B * A * B A ¬ A < B
13 12 biimpar B * A * ¬ A < B B A
14 9 10 11 13 syl21anc A * B * C * ¬ A < B B A
15 3ancoma B * A * C * A * B * C *
16 incom B C A C = A C B C
17 iocinioc2 B * A * C * B A B C A C = A C
18 16 17 eqtr3id B * A * C * B A A C B C = A C
19 15 18 sylanbr A * B * C * B A A C B C = A C
20 14 19 syldan A * B * C * ¬ A < B A C B C = A C
21 20 ex A * B * C * ¬ A < B A C B C = A C
22 21 ancld A * B * C * ¬ A < B ¬ A < B A C B C = A C
23 8 22 orim12d A * B * C * A < B ¬ A < B A < B A C B C = B C ¬ A < B A C B C = A C
24 1 23 mpi A * B * C * A < B A C B C = B C ¬ A < B A C B C = A C
25 eqif A C B C = if A < B B C A C A < B A C B C = B C ¬ A < B A C B C = A C
26 24 25 sylibr A * B * C * A C B C = if A < B B C A C