Description: A real number smaller than or equal to the lower bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lenelioc.1 | ||
lenelioc.2 | |||
lenelioc.3 | |||
lenelioc.4 | |||
Assertion | lenelioc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lenelioc.1 | ||
2 | lenelioc.2 | ||
3 | lenelioc.3 | ||
4 | lenelioc.4 | ||
5 | 3 1 | xrlenltd | |
6 | 4 5 | mpbid | |
7 | 6 | intn3an2d | |
8 | elioc1 | ||
9 | 1 2 8 | syl2anc | |
10 | 7 9 | mtbird |