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 ) )