Theorem gtnelioc

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

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

Proof

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