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 e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B < C ) -> ( ( A [,] B ) i^i ( C [,] D ) ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		simplll	|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B < C ) -> A e. RR* )
2		simplrr	|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B < C ) -> D e. RR* )
3		simpr	|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B < C ) -> B < C )
4		iccdisj2	|- ( ( A e. RR* /\ D e. RR* /\ B < C ) -> ( ( A [,] B ) i^i ( C [,] D ) ) = (/) )
5	1 2 3 4	syl3anc	|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B < C ) -> ( ( A [,] B ) i^i ( C [,] D ) ) = (/) )