Metamath Proof Explorer


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 )