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 ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ*𝐷 ∈ ℝ* ) ) ∧ 𝐵 < 𝐶 ) → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐶 [,] 𝐷 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 simplll ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ*𝐷 ∈ ℝ* ) ) ∧ 𝐵 < 𝐶 ) → 𝐴 ∈ ℝ* )
2 simplrr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ*𝐷 ∈ ℝ* ) ) ∧ 𝐵 < 𝐶 ) → 𝐷 ∈ ℝ* )
3 simpr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ*𝐷 ∈ ℝ* ) ) ∧ 𝐵 < 𝐶 ) → 𝐵 < 𝐶 )
4 iccdisj2 ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐶 [,] 𝐷 ) ) = ∅ )
5 1 2 3 4 syl3anc ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ*𝐷 ∈ ℝ* ) ) ∧ 𝐵 < 𝐶 ) → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐶 [,] 𝐷 ) ) = ∅ )