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 \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{})) \land B < C) \to [A, B] \cap [C, D] = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		simplll	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{})) \land B < C) \to A \in ℝ^{*}$
2		simplrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{})) \land B < C) \to D \in ℝ^{*}$
3		simpr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{})) \land B < C) \to B < C$
4		iccdisj2	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to [A, B] \cap [C, D] = \emptyset$
5	1 2 3 4	syl3anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{})) \land B < C) \to [A, B] \cap [C, D] = \emptyset$