Metamath Proof Explorer


Theorem iccdisj2

Description: If the upper bound of one closed interval is less than the lower bound of the other, the intervals are disjoint. (Contributed by Zhi Wang, 9-Sep-2024)

Ref Expression
Assertion iccdisj2 A * D * B < C A B C D =

Proof

Step Hyp Ref Expression
1 simp1 A * D * B < C A *
2 simp3 A * D * B < C B < C
3 ltrelxr < * × *
4 3 brel B < C B * C *
5 2 4 syl A * D * B < C B * C *
6 5 simprd A * D * B < C C *
7 1 xrleidd A * D * B < C A A
8 iccssico A * C * A A B < C A B A C
9 1 6 7 2 8 syl22anc A * D * B < C A B A C
10 simp2 A * D * B < C D *
11 df-ico . = x * , y * z * | x z z < y
12 df-icc . = x * , y * z * | x z z y
13 xrlenlt C * w * C w ¬ w < C
14 11 12 13 ixxdisj A * C * D * A C C D =
15 1 6 10 14 syl3anc A * D * B < C A C C D =
16 9 15 ssdisjd A * D * B < C A B C D =