Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐴 ∈ ℝ* ) |
2 |
|
icossxr |
⊢ ( 𝐴 [,) 𝐵 ) ⊆ ℝ* |
3 |
|
id |
⊢ ( 𝐵 ∈ ( 𝐴 [,) 𝐵 ) → 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) |
4 |
2 3
|
sseldi |
⊢ ( 𝐵 ∈ ( 𝐴 [,) 𝐵 ) → 𝐵 ∈ ℝ* ) |
5 |
4
|
adantl |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 ∈ ℝ* ) |
6 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) |
7 |
|
icoltub |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 < 𝐵 ) |
8 |
1 5 6 7
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 < 𝐵 ) |
9 |
|
xrltnr |
⊢ ( 𝐵 ∈ ℝ* → ¬ 𝐵 < 𝐵 ) |
10 |
4 9
|
syl |
⊢ ( 𝐵 ∈ ( 𝐴 [,) 𝐵 ) → ¬ 𝐵 < 𝐵 ) |
11 |
10
|
adantl |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → ¬ 𝐵 < 𝐵 ) |
12 |
8 11
|
pm2.65da |
⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) |