Description: A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | ioondisj2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll1 | |
|
2 | simpll2 | |
|
3 | simplr1 | |
|
4 | simplr2 | |
|
5 | iooin | |
|
6 | 1 2 3 4 5 | syl22anc | |
7 | simprr | |
|
8 | xrmineq | |
|
9 | 2 4 7 8 | syl3anc | |
10 | 9 | oveq2d | |
11 | simpr | |
|
12 | 11 | iftrued | |
13 | simplr3 | |
|
14 | 13 | adantr | |
15 | 12 14 | eqbrtrd | |
16 | simpr | |
|
17 | 16 | iffalsed | |
18 | simplrl | |
|
19 | 17 18 | eqbrtrd | |
20 | 15 19 | pm2.61dan | |
21 | 3 1 | ifcld | |
22 | ioon0 | |
|
23 | 21 4 22 | syl2anc | |
24 | 20 23 | mpbird | |
25 | 10 24 | eqnetrd | |
26 | 6 25 | eqnetrd | |