Metamath Proof Explorer

Theorem eliccelico

Description: Relate elementhood to a closed interval with elementhood to the same closed-below, open-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017)

Ref Expression
Assertion eliccelico 
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( C e. ( A [,] B ) <-> ( C e. ( A [,) B ) \/ C = B ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) ) -> A e. RR* )
2 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) ) -> B e. RR* )
3 simprl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) ) -> C e. ( A [,] B ) )
4 elicc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ A <_ C /\ C <_ B ) ) )
5 4 biimpa 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. ( A [,] B ) ) -> ( C e. RR* /\ A <_ C /\ C <_ B ) )
6 5 simp1d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. ( A [,] B ) ) -> C e. RR* )
7 1 2 3 6 syl21anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) ) -> C e. RR* )
8 5 simp3d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. ( A [,] B ) ) -> C <_ B )
9 1 2 3 8 syl21anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) ) -> C <_ B )
10 1 2 jca 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) ) -> ( A e. RR* /\ B e. RR* ) )
11 simprr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) ) -> -. C e. ( A [,) B ) )
12 5 simp2d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. ( A [,] B ) ) -> A <_ C )
13 10 3 12 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) ) -> A <_ C )
14 elico1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR* /\ A <_ C /\ C < B ) ) )
15 14 notbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. C e. ( A [,) B ) <-> -. ( C e. RR* /\ A <_ C /\ C < B ) ) )
16 15 biimpa 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. C e. ( A [,) B ) ) -> -. ( C e. RR* /\ A <_ C /\ C < B ) )
17 df-3an 
 |-  ( ( C e. RR* /\ A <_ C /\ C < B ) <-> ( ( C e. RR* /\ A <_ C ) /\ C < B ) )
18 17 notbii 
 |-  ( -. ( C e. RR* /\ A <_ C /\ C < B ) <-> -. ( ( C e. RR* /\ A <_ C ) /\ C < B ) )
19 imnan 
 |-  ( ( ( C e. RR* /\ A <_ C ) -> -. C < B ) <-> -. ( ( C e. RR* /\ A <_ C ) /\ C < B ) )
20 18 19 bitr4i 
 |-  ( -. ( C e. RR* /\ A <_ C /\ C < B ) <-> ( ( C e. RR* /\ A <_ C ) -> -. C < B ) )
21 16 20 sylib 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. C e. ( A [,) B ) ) -> ( ( C e. RR* /\ A <_ C ) -> -. C < B ) )
22 21 imp 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. C e. ( A [,) B ) ) /\ ( C e. RR* /\ A <_ C ) ) -> -. C < B )
23 10 11 7 13 22 syl22anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) ) -> -. C < B )
24 xeqlelt 
 |-  ( ( C e. RR* /\ B e. RR* ) -> ( C = B <-> ( C <_ B /\ -. C < B ) ) )
25 24 biimpar 
 |-  ( ( ( C e. RR* /\ B e. RR* ) /\ ( C <_ B /\ -. C < B ) ) -> C = B )
26 7 2 9 23 25 syl22anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) ) -> C = B )
27 26 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) -> C = B ) )
28 pm5.6 
 |-  ( ( ( C e. ( A [,] B ) /\ -. C e. ( A [,) B ) ) -> C = B ) <-> ( C e. ( A [,] B ) -> ( C e. ( A [,) B ) \/ C = B ) ) )
29 27 28 sylib 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( C e. ( A [,] B ) -> ( C e. ( A [,) B ) \/ C = B ) ) )
30 icossicc 
 |-  ( A [,) B ) C_ ( A [,] B )
31 simpr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C e. ( A [,) B ) ) -> C e. ( A [,) B ) )
32 30 31 sselid 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C e. ( A [,) B ) ) -> C e. ( A [,] B ) )
33 simpr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> C = B )
34 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> B e. RR* )
35 33 34 eqeltrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> C e. RR* )
36 simpl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> A <_ B )
37 36 33 breqtrrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> A <_ C )
38 34 xrleidd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> B <_ B )
39 33 38 eqbrtrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> C <_ B )
40 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> A e. RR* )
41 40 34 4 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ A <_ C /\ C <_ B ) ) )
42 35 37 39 41 mpbir3and 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> C e. ( A [,] B ) )
43 32 42 jaodan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C e. ( A [,) B ) \/ C = B ) ) -> C e. ( A [,] B ) )
44 43 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( C e. ( A [,) B ) \/ C = B ) -> C e. ( A [,] B ) ) )
45 29 44 impbid 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( C e. ( A [,] B ) <-> ( C e. ( A [,) B ) \/ C = B ) ) )