This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> A e. RR* )
lenelioc.2 
|- ( ph -> B e. RR* )
lenelioc.3 
|- ( ph -> C e. RR* )
lenelioc.4 
|- ( ph -> C <_ A )
Assertion lenelioc 
|- ( ph -> -. C e. ( A (,] B ) )

Proof

Step Hyp Ref Expression
1 lenelioc.1 
 |-  ( ph -> A e. RR* )
2 lenelioc.2 
 |-  ( ph -> B e. RR* )
3 lenelioc.3 
 |-  ( ph -> C e. RR* )
4 lenelioc.4 
 |-  ( ph -> C <_ A )
5 3 1 xrlenltd 
 |-  ( ph -> ( C <_ A <-> -. A < C ) )
6 4 5 mpbid 
 |-  ( ph -> -. A < C )
7 6 intn3an2d 
 |-  ( ph -> -. ( C e. RR* /\ A < C /\ C <_ B ) )
8 elioc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,] B ) <-> ( C e. RR* /\ A < C /\ C <_ B ) ) )
9 1 2 8 syl2anc 
 |-  ( ph -> ( C e. ( A (,] B ) <-> ( C e. RR* /\ A < C /\ C <_ B ) ) )
10 7 9 mtbird 
 |-  ( ph -> -. C e. ( A (,] B ) )