Description: A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | icoub | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | icossxr | |
|
3 | id | |
|
4 | 2 3 | sselid | |
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 | |