Theorem eliccnelico

Description: An element of a closed interval that is not a member of the left-closed right-open interval, must be the upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	eliccnelico.1	|- ( ph -> A e. RR* )
	eliccnelico.b	|- ( ph -> B e. RR* )
	eliccnelico.c	|- ( ph -> C e. ( A [,] B ) )
	eliccnelico.nel	|- ( ph -> -. C e. ( A [,) B ) )
Assertion	eliccnelico	|- ( ph -> C = B )

Proof

Step	Hyp	Ref	Expression
1		eliccnelico.1	|- ( ph -> A e. RR* )
2		eliccnelico.b	|- ( ph -> B e. RR* )
3		eliccnelico.c	|- ( ph -> C e. ( A [,] B ) )
4		eliccnelico.nel	|- ( ph -> -. C e. ( A [,) B ) )
5		eliccxr	|- ( C e. ( A [,] B ) -> C e. RR* )
6	3 5	syl	|- ( ph -> C e. RR* )
7		iccleub	|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> C <_ B )
8	1 2 3 7	syl3anc	|- ( ph -> C <_ B )
9	1	adantr	|- ( ( ph /\ -. B <_ C ) -> A e. RR* )
10	2	adantr	|- ( ( ph /\ -. B <_ C ) -> B e. RR* )
11	6	adantr	|- ( ( ph /\ -. B <_ C ) -> C e. RR* )
12		iccgelb	|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> A <_ C )
13	1 2 3 12	syl3anc	|- ( ph -> A <_ C )
14	13	adantr	|- ( ( ph /\ -. B <_ C ) -> A <_ C )
15		simpr	|- ( ( ph /\ -. B <_ C ) -> -. B <_ C )
16		xrltnle	|- ( ( C e. RR* /\ B e. RR* ) -> ( C < B <-> -. B <_ C ) )
17	6 2 16	syl2anc	|- ( ph -> ( C < B <-> -. B <_ C ) )
18	17	adantr	|- ( ( ph /\ -. B <_ C ) -> ( C < B <-> -. B <_ C ) )
19	15 18	mpbird	|- ( ( ph /\ -. B <_ C ) -> C < B )
20	9 10 11 14 19	elicod	|- ( ( ph /\ -. B <_ C ) -> C e. ( A [,) B ) )
21	4	adantr	|- ( ( ph /\ -. B <_ C ) -> -. C e. ( A [,) B ) )
22	20 21	condan	|- ( ph -> B <_ C )
23	6 2 8 22	xrletrid	|- ( ph -> C = B )