Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → 𝐴 ∈ ℝ* ) |
2 |
|
simp3 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → 𝐵 < 𝐶 ) |
3 |
|
ltrelxr |
⊢ < ⊆ ( ℝ* × ℝ* ) |
4 |
3
|
brel |
⊢ ( 𝐵 < 𝐶 → ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ) |
5 |
2 4
|
syl |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ) |
6 |
5
|
simprd |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → 𝐶 ∈ ℝ* ) |
7 |
1
|
xrleidd |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → 𝐴 ≤ 𝐴 ) |
8 |
|
iccssico |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐵 < 𝐶 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,) 𝐶 ) ) |
9 |
1 6 7 2 8
|
syl22anc |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,) 𝐶 ) ) |
10 |
|
simp2 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → 𝐷 ∈ ℝ* ) |
11 |
|
df-ico |
⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) |
12 |
|
df-icc |
⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ) |
13 |
|
xrlenlt |
⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐶 ≤ 𝑤 ↔ ¬ 𝑤 < 𝐶 ) ) |
14 |
11 12 13
|
ixxdisj |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐶 ) ∩ ( 𝐶 [,] 𝐷 ) ) = ∅ ) |
15 |
1 6 10 14
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → ( ( 𝐴 [,) 𝐶 ) ∩ ( 𝐶 [,] 𝐷 ) ) = ∅ ) |
16 |
9 15
|
ssdisjd |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐶 [,] 𝐷 ) ) = ∅ ) |