Theorem ltnelicc

Description: A real number smaller than the lower bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	ltnelicc.a	|- ( ph -> A e. RR )
	ltnelicc.b	|- ( ph -> B e. RR* )
	ltnelicc.c	|- ( ph -> C e. RR* )
	ltnelicc.clta	|- ( ph -> C < A )
Assertion	ltnelicc	|- ( ph -> -. C e. ( A [,] B ) )

Proof

Step	Hyp	Ref	Expression
1		ltnelicc.a	|- ( ph -> A e. RR )
2		ltnelicc.b	|- ( ph -> B e. RR* )
3		ltnelicc.c	|- ( ph -> C e. RR* )
4		ltnelicc.clta	|- ( ph -> C < A )
5	1	rexrd	|- ( ph -> A e. RR* )
6		xrltnle	|- ( ( C e. RR* /\ A e. RR* ) -> ( C < A <-> -. A <_ C ) )
7	3 5 6	syl2anc	|- ( ph -> ( C < A <-> -. A <_ C ) )
8	4 7	mpbid	|- ( ph -> -. A <_ C )
9	8	intnanrd	|- ( ph -> -. ( A <_ C /\ C <_ B ) )
10		elicc4	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )
11	5 2 3 10	syl3anc	|- ( ph -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )
12	9 11	mtbird	|- ( ph -> -. C e. ( A [,] B ) )