Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( A e. RR* /\ B e. ( A [,) B ) ) -> A e. RR* ) |
2 |
|
icossxr |
|- ( A [,) B ) C_ RR* |
3 |
|
id |
|- ( B e. ( A [,) B ) -> B e. ( A [,) B ) ) |
4 |
2 3
|
sseldi |
|- ( B e. ( A [,) B ) -> B e. RR* ) |
5 |
4
|
adantl |
|- ( ( A e. RR* /\ B e. ( A [,) B ) ) -> B e. RR* ) |
6 |
|
simpr |
|- ( ( A e. RR* /\ B e. ( A [,) B ) ) -> B e. ( A [,) B ) ) |
7 |
|
icoltub |
|- ( ( A e. RR* /\ B e. RR* /\ B e. ( A [,) B ) ) -> B < B ) |
8 |
1 5 6 7
|
syl3anc |
|- ( ( A e. RR* /\ B e. ( A [,) B ) ) -> B < B ) |
9 |
|
xrltnr |
|- ( B e. RR* -> -. B < B ) |
10 |
4 9
|
syl |
|- ( B e. ( A [,) B ) -> -. B < B ) |
11 |
10
|
adantl |
|- ( ( A e. RR* /\ B e. ( A [,) B ) ) -> -. B < B ) |
12 |
8 11
|
pm2.65da |
|- ( A e. RR* -> -. B e. ( A [,) B ) ) |