Description: The difference between two open intervals sharing the same lower bound. (Contributed by Thierry Arnoux, 26-Sep-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | difioo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | incom | |
|
2 | joiniooico | |
|
3 | 2 | anassrs | |
4 | 3 | simpld | |
5 | 1 4 | eqtr3id | |
6 | 3 | simprd | |
7 | uncom | |
|
8 | 7 | a1i | |
9 | simpll1 | |
|
10 | simpl3 | |
|
11 | 10 | adantr | |
12 | 9 | xrleidd | |
13 | simpr | |
|
14 | ioossioo | |
|
15 | 9 11 12 13 14 | syl22anc | |
16 | ssequn2 | |
|
17 | 15 16 | sylib | |
18 | 6 8 17 | 3eqtr4d | |
19 | difeq | |
|
20 | 5 18 19 | sylanbrc | |
21 | simpll1 | |
|
22 | simpl2 | |
|
23 | 22 | adantr | |
24 | 21 | xrleidd | |
25 | 10 | adantr | |
26 | simpr | |
|
27 | 25 23 26 | xrltled | |
28 | ioossioo | |
|
29 | 21 23 24 27 28 | syl22anc | |
30 | ssdif0 | |
|
31 | 29 30 | sylib | |
32 | ico0 | |
|
33 | 32 | biimpar | |
34 | 23 25 27 33 | syl21anc | |
35 | 31 34 | eqtr4d | |
36 | xrlelttric | |
|
37 | 22 10 36 | syl2anc | |
38 | 20 35 37 | mpjaodan | |