eliccelioc

Description: Membership in a closed interval and in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		eliccelioc.a	\|- ( ph -> A e. RR )
2		eliccelioc.b	\|- ( ph -> B e. RR )
3		eliccelioc.c	\|- ( ph -> C e. RR* )
4		iocssicc	\|- ( A (,] B ) C_ ( A [,] B )
5	4	sseli	\|- ( C e. ( A (,] B ) -> C e. ( A [,] B ) )
6	5	adantl	\|- ( ( ph /\ C e. ( A (,] B ) ) -> C e. ( A [,] B ) )
7	1	adantr	\|- ( ( ph /\ C e. ( A (,] B ) ) -> A e. RR )
8	1	rexrd	\|- ( ph -> A e. RR* )
9	8	adantr	\|- ( ( ph /\ C e. ( A (,] B ) ) -> A e. RR* )
10	2	adantr	\|- ( ( ph /\ C e. ( A (,] B ) ) -> B e. RR )
11	10	rexrd	\|- ( ( ph /\ C e. ( A (,] B ) ) -> B e. RR* )
12		simpr	\|- ( ( ph /\ C e. ( A (,] B ) ) -> C e. ( A (,] B ) )
13		iocgtlb	\|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A (,] B ) ) -> A < C )
14	9 11 12 13	syl3anc	\|- ( ( ph /\ C e. ( A (,] B ) ) -> A < C )
15	7 14	gtned	\|- ( ( ph /\ C e. ( A (,] B ) ) -> C =/= A )
16	6 15	jca	\|- ( ( ph /\ C e. ( A (,] B ) ) -> ( C e. ( A [,] B ) /\ C =/= A ) )
17	8	adantr	\|- ( ( ph /\ ( C e. ( A [,] B ) /\ C =/= A ) ) -> A e. RR* )
18	2	rexrd	\|- ( ph -> B e. RR* )
19	18	adantr	\|- ( ( ph /\ ( C e. ( A [,] B ) /\ C =/= A ) ) -> B e. RR* )
20	3	adantr	\|- ( ( ph /\ ( C e. ( A [,] B ) /\ C =/= A ) ) -> C e. RR* )
21	1	adantr	\|- ( ( ph /\ ( C e. ( A [,] B ) /\ C =/= A ) ) -> A e. RR )
22	1 2	iccssred	\|- ( ph -> ( A [,] B ) C_ RR )
23	22	sselda	\|- ( ( ph /\ C e. ( A [,] B ) ) -> C e. RR )
24	23	adantrr	\|- ( ( ph /\ ( C e. ( A [,] B ) /\ C =/= A ) ) -> C e. RR )
25	8	adantr	\|- ( ( ph /\ C e. ( A [,] B ) ) -> A e. RR* )
26	18	adantr	\|- ( ( ph /\ C e. ( A [,] B ) ) -> B e. RR* )
27		simpr	\|- ( ( ph /\ C e. ( A [,] B ) ) -> C e. ( A [,] B ) )
28		iccgelb	\|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> A <_ C )
29	25 26 27 28	syl3anc	\|- ( ( ph /\ C e. ( A [,] B ) ) -> A <_ C )
30	29	adantrr	\|- ( ( ph /\ ( C e. ( A [,] B ) /\ C =/= A ) ) -> A <_ C )
31		simprr	\|- ( ( ph /\ ( C e. ( A [,] B ) /\ C =/= A ) ) -> C =/= A )
32	21 24 30 31	leneltd	\|- ( ( ph /\ ( C e. ( A [,] B ) /\ C =/= A ) ) -> A < C )
33		iccleub	\|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> C <_ B )
34	25 26 27 33	syl3anc	\|- ( ( ph /\ C e. ( A [,] B ) ) -> C <_ B )
35	34	adantrr	\|- ( ( ph /\ ( C e. ( A [,] B ) /\ C =/= A ) ) -> C <_ B )
36	17 19 20 32 35	eliocd	\|- ( ( ph /\ ( C e. ( A [,] B ) /\ C =/= A ) ) -> C e. ( A (,] B ) )
37	16 36	impbida	\|- ( ph -> ( C e. ( A (,] B ) <-> ( C e. ( A [,] B ) /\ C =/= A ) ) )

Metamath Proof Explorer

Theorem eliccelioc

Proof