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

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 )