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

Proof

Step Hyp Ref Expression
1 incom ABBC=BCAB
2 joiniooico A*B*C*A<BBCABBC=ABBC=AC
3 2 anassrs A*B*C*A<BBCABBC=ABBC=AC
4 3 simpld A*B*C*A<BBCABBC=
5 1 4 eqtr3id A*B*C*A<BBCBCAB=
6 3 simprd A*B*C*A<BBCABBC=AC
7 uncom BCAB=ABBC
8 7 a1i A*B*C*A<BBCBCAB=ABBC
9 simpll1 A*B*C*A<BBCA*
10 simpl3 A*B*C*A<BC*
11 10 adantr A*B*C*A<BBCC*
12 9 xrleidd A*B*C*A<BBCAA
13 simpr A*B*C*A<BBCBC
14 ioossioo A*C*AABCABAC
15 9 11 12 13 14 syl22anc A*B*C*A<BBCABAC
16 ssequn2 ABACACAB=AC
17 15 16 sylib A*B*C*A<BBCACAB=AC
18 6 8 17 3eqtr4d A*B*C*A<BBCBCAB=ACAB
19 difeq ACAB=BCBCAB=BCAB=ACAB
20 5 18 19 sylanbrc A*B*C*A<BBCACAB=BC
21 simpll1 A*B*C*A<BC<BA*
22 simpl2 A*B*C*A<BB*
23 22 adantr A*B*C*A<BC<BB*
24 21 xrleidd A*B*C*A<BC<BAA
25 10 adantr A*B*C*A<BC<BC*
26 simpr A*B*C*A<BC<BC<B
27 25 23 26 xrltled A*B*C*A<BC<BCB
28 ioossioo A*B*AACBACAB
29 21 23 24 27 28 syl22anc A*B*C*A<BC<BACAB
30 ssdif0 ACABACAB=
31 29 30 sylib A*B*C*A<BC<BACAB=
32 ico0 B*C*BC=CB
33 32 biimpar B*C*CBBC=
34 23 25 27 33 syl21anc A*B*C*A<BC<BBC=
35 31 34 eqtr4d A*B*C*A<BC<BACAB=BC
36 xrlelttric B*C*BCC<B
37 22 10 36 syl2anc A*B*C*A<BBCC<B
38 20 35 37 mpjaodan A*B*C*A<BACAB=BC