Theorem xrgtnelicc

Description: A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	xrgtnelicc.1	|- ( ph -> A e. RR* )
	xrgtnelicc.2	|- ( ph -> B e. RR* )
	xrgtnelicc.3	|- ( ph -> C e. RR* )
	xrgtnelicc.4	|- ( ph -> B < C )
Assertion	xrgtnelicc	|- ( ph -> -. C e. ( A [,] B ) )

Proof

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