Metamath Proof Explorer


Theorem iccdisj

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 iccdisj A * B * C * D * B < C A B C D =

Proof

Step Hyp Ref Expression
1 simplll A * B * C * D * B < C A *
2 simplrr A * B * C * D * B < C D *
3 simpr A * B * C * D * B < C B < C
4 iccdisj2 A * D * B < C A B C D =
5 1 2 3 4 syl3anc A * B * C * D * B < C A B C D =