Metamath Proof Explorer


Theorem ioondisj2

Description: A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion ioondisj2 A*B*A<BC*D*C<DA<DDBABCD

Proof

Step Hyp Ref Expression
1 simpll1 A*B*A<BC*D*C<DA<DDBA*
2 simpll2 A*B*A<BC*D*C<DA<DDBB*
3 simplr1 A*B*A<BC*D*C<DA<DDBC*
4 simplr2 A*B*A<BC*D*C<DA<DDBD*
5 iooin A*B*C*D*ABCD=ifACCAifBDBD
6 1 2 3 4 5 syl22anc A*B*A<BC*D*C<DA<DDBABCD=ifACCAifBDBD
7 simprr A*B*A<BC*D*C<DA<DDBDB
8 xrmineq B*D*DBifBDBD=D
9 2 4 7 8 syl3anc A*B*A<BC*D*C<DA<DDBifBDBD=D
10 9 oveq2d A*B*A<BC*D*C<DA<DDBifACCAifBDBD=ifACCAD
11 simpr A*B*A<BC*D*C<DA<DDBACAC
12 11 iftrued A*B*A<BC*D*C<DA<DDBACifACCA=C
13 simplr3 A*B*A<BC*D*C<DA<DDBC<D
14 13 adantr A*B*A<BC*D*C<DA<DDBACC<D
15 12 14 eqbrtrd A*B*A<BC*D*C<DA<DDBACifACCA<D
16 simpr A*B*A<BC*D*C<DA<DDB¬AC¬AC
17 16 iffalsed A*B*A<BC*D*C<DA<DDB¬ACifACCA=A
18 simplrl A*B*A<BC*D*C<DA<DDB¬ACA<D
19 17 18 eqbrtrd A*B*A<BC*D*C<DA<DDB¬ACifACCA<D
20 15 19 pm2.61dan A*B*A<BC*D*C<DA<DDBifACCA<D
21 3 1 ifcld A*B*A<BC*D*C<DA<DDBifACCA*
22 ioon0 ifACCA*D*ifACCADifACCA<D
23 21 4 22 syl2anc A*B*A<BC*D*C<DA<DDBifACCADifACCA<D
24 20 23 mpbird A*B*A<BC*D*C<DA<DDBifACCAD
25 10 24 eqnetrd A*B*A<BC*D*C<DA<DDBifACCAifBDBD
26 6 25 eqnetrd A*B*A<BC*D*C<DA<DDBABCD