Metamath Proof Explorer


Theorem ioondisj1

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

Ref Expression
Assertion ioondisj1 A*B*A<BC*D*C<DACC<BABCD

Proof

Step Hyp Ref Expression
1 simpll1 A*B*A<BC*D*C<DACC<BA*
2 simpll2 A*B*A<BC*D*C<DACC<BB*
3 simplr1 A*B*A<BC*D*C<DACC<BC*
4 simplr2 A*B*A<BC*D*C<DACC<BD*
5 iooin A*B*C*D*ABCD=ifACCAifBDBD
6 1 2 3 4 5 syl22anc A*B*A<BC*D*C<DACC<BABCD=ifACCAifBDBD
7 simprl A*B*A<BC*D*C<DACC<BAC
8 7 iftrued A*B*A<BC*D*C<DACC<BifACCA=C
9 8 oveq1d A*B*A<BC*D*C<DACC<BifACCAifBDBD=CifBDBD
10 simprr A*B*A<BC*D*C<DACC<BC<B
11 simplr3 A*B*A<BC*D*C<DACC<BC<D
12 10 11 jca A*B*A<BC*D*C<DACC<BC<BC<D
13 xrltmin C*B*D*C<ifBDBDC<BC<D
14 3 2 4 13 syl3anc A*B*A<BC*D*C<DACC<BC<ifBDBDC<BC<D
15 12 14 mpbird A*B*A<BC*D*C<DACC<BC<ifBDBD
16 2 4 ifcld A*B*A<BC*D*C<DACC<BifBDBD*
17 ioon0 C*ifBDBD*CifBDBDC<ifBDBD
18 3 16 17 syl2anc A*B*A<BC*D*C<DACC<BCifBDBDC<ifBDBD
19 15 18 mpbird A*B*A<BC*D*C<DACC<BCifBDBD
20 9 19 eqnetrd A*B*A<BC*D*C<DACC<BifACCAifBDBD
21 6 20 eqnetrd A*B*A<BC*D*C<DACC<BABCD