This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ) ) )