Metamath Proof Explorer


Theorem lenelioc

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 φ A *
lenelioc.2 φ B *
lenelioc.3 φ C *
lenelioc.4 φ C A
Assertion lenelioc φ ¬ C A B

Proof

Step Hyp Ref Expression
1 lenelioc.1 φ A *
2 lenelioc.2 φ B *
3 lenelioc.3 φ C *
4 lenelioc.4 φ C A
5 3 1 xrlenltd φ C A ¬ A < C
6 4 5 mpbid φ ¬ A < C
7 6 intn3an2d φ ¬ C * A < C C B
8 elioc1 A * B * C A B C * A < C C B
9 1 2 8 syl2anc φ C A B C * A < C C B
10 7 9 mtbird φ ¬ C A B