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