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

Metamath Proof Explorer

Theorem eliccelicod

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

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

Proof

Step Hyp Ref Expression
1 eliccelicod.a 
 |-  ( ph -> A e. RR* )
2 eliccelicod.b 
 |-  ( ph -> B e. RR* )
3 eliccelicod.c 
 |-  ( ph -> C e. ( A [,] B ) )
4 eliccelicod.d 
 |-  ( ph -> C =/= B )
5 eliccxr 
 |-  ( C e. ( A [,] B ) -> C e. RR* )
6 3 5 syl 
 |-  ( ph -> C e. RR* )
7 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> A <_ C )
8 1 2 3 7 syl3anc 
 |-  ( ph -> A <_ C )
9 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> C <_ B )
10 1 2 3 9 syl3anc 
 |-  ( ph -> C <_ B )
11 6 2 10 4 xrleneltd 
 |-  ( ph -> C < B )
12 1 2 6 8 11 elicod 
 |-  ( ph -> C e. ( A [,) B ) )