Metamath Proof Explorer

Theorem elicc3

Description: An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009)

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

Proof

Step Hyp Ref Expression
1 elicc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ A <_ C /\ C <_ B ) ) )
2 simp1 
 |-  ( ( C e. RR* /\ A <_ C /\ C <_ B ) -> C e. RR* )
3 2 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ C /\ C <_ B ) -> C e. RR* ) )
4 xrletr 
 |-  ( ( A e. RR* /\ C e. RR* /\ B e. RR* ) -> ( ( A <_ C /\ C <_ B ) -> A <_ B ) )
5 4 exp5o 
 |-  ( A e. RR* -> ( C e. RR* -> ( B e. RR* -> ( A <_ C -> ( C <_ B -> A <_ B ) ) ) ) )
6 5 com23 
 |-  ( A e. RR* -> ( B e. RR* -> ( C e. RR* -> ( A <_ C -> ( C <_ B -> A <_ B ) ) ) ) )
7 6 imp5q 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ C /\ C <_ B ) -> A <_ B ) )
8 df-ne 
 |-  ( C =/= A <-> -. C = A )
9 xrleltne 
 |-  ( ( A e. RR* /\ C e. RR* /\ A <_ C ) -> ( A < C <-> C =/= A ) )
10 9 biimprd 
 |-  ( ( A e. RR* /\ C e. RR* /\ A <_ C ) -> ( C =/= A -> A < C ) )
11 8 10 syl5bir 
 |-  ( ( A e. RR* /\ C e. RR* /\ A <_ C ) -> ( -. C = A -> A < C ) )
12 11 3adant3r3 
 |-  ( ( A e. RR* /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> ( -. C = A -> A < C ) )
13 12 adantlr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> ( -. C = A -> A < C ) )
14 eqcom 
 |-  ( C = B <-> B = C )
15 14 necon3bbii 
 |-  ( -. C = B <-> B =/= C )
16 xrleltne 
 |-  ( ( C e. RR* /\ B e. RR* /\ C <_ B ) -> ( C < B <-> B =/= C ) )
17 16 biimprd 
 |-  ( ( C e. RR* /\ B e. RR* /\ C <_ B ) -> ( B =/= C -> C < B ) )
18 15 17 syl5bi 
 |-  ( ( C e. RR* /\ B e. RR* /\ C <_ B ) -> ( -. C = B -> C < B ) )
19 18 3exp 
 |-  ( C e. RR* -> ( B e. RR* -> ( C <_ B -> ( -. C = B -> C < B ) ) ) )
20 19 com12 
 |-  ( B e. RR* -> ( C e. RR* -> ( C <_ B -> ( -. C = B -> C < B ) ) ) )
21 20 imp32 
 |-  ( ( B e. RR* /\ ( C e. RR* /\ C <_ B ) ) -> ( -. C = B -> C < B ) )
22 21 3adantr2 
 |-  ( ( B e. RR* /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> ( -. C = B -> C < B ) )
23 22 adantll 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> ( -. C = B -> C < B ) )
24 13 23 anim12d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> ( ( -. C = A /\ -. C = B ) -> ( A < C /\ C < B ) ) )
25 24 ex 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ C /\ C <_ B ) -> ( ( -. C = A /\ -. C = B ) -> ( A < C /\ C < B ) ) ) )
26 df-or 
 |-  ( ( C = A \/ ( ( A < C /\ C < B ) \/ C = B ) ) <-> ( -. C = A -> ( ( A < C /\ C < B ) \/ C = B ) ) )
27 3orass 
 |-  ( ( C = A \/ ( A < C /\ C < B ) \/ C = B ) <-> ( C = A \/ ( ( A < C /\ C < B ) \/ C = B ) ) )
28 pm5.6 
 |-  ( ( ( -. C = A /\ -. C = B ) -> ( A < C /\ C < B ) ) <-> ( -. C = A -> ( C = B \/ ( A < C /\ C < B ) ) ) )
29 orcom 
 |-  ( ( C = B \/ ( A < C /\ C < B ) ) <-> ( ( A < C /\ C < B ) \/ C = B ) )
30 29 imbi2i 
 |-  ( ( -. C = A -> ( C = B \/ ( A < C /\ C < B ) ) ) <-> ( -. C = A -> ( ( A < C /\ C < B ) \/ C = B ) ) )
31 28 30 bitri 
 |-  ( ( ( -. C = A /\ -. C = B ) -> ( A < C /\ C < B ) ) <-> ( -. C = A -> ( ( A < C /\ C < B ) \/ C = B ) ) )
32 26 27 31 3bitr4ri 
 |-  ( ( ( -. C = A /\ -. C = B ) -> ( A < C /\ C < B ) ) <-> ( C = A \/ ( A < C /\ C < B ) \/ C = B ) )
33 25 32 syl6ib 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ C /\ C <_ B ) -> ( C = A \/ ( A < C /\ C < B ) \/ C = B ) ) )
34 3 7 33 3jcad 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ C /\ C <_ B ) -> ( C e. RR* /\ A <_ B /\ ( C = A \/ ( A < C /\ C < B ) \/ C = B ) ) ) )
35 simp1 
 |-  ( ( C e. RR* /\ A <_ B /\ ( C = A \/ ( A < C /\ C < B ) \/ C = B ) ) -> C e. RR* )
36 35 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ B /\ ( C = A \/ ( A < C /\ C < B ) \/ C = B ) ) -> C e. RR* ) )
37 xrleid 
 |-  ( A e. RR* -> A <_ A )
38 37 ad3antrrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> A <_ A )
39 breq2 
 |-  ( C = A -> ( A <_ C <-> A <_ A ) )
40 38 39 syl5ibrcom 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> ( C = A -> A <_ C ) )
41 xrltle 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A < C -> A <_ C ) )
42 41 adantr 
 |-  ( ( ( A e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( A < C -> A <_ C ) )
43 42 adantllr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> ( A < C -> A <_ C ) )
44 43 adantrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> ( ( A < C /\ C < B ) -> A <_ C ) )
45 simpr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> A <_ B )
46 breq2 
 |-  ( C = B -> ( A <_ C <-> A <_ B ) )
47 45 46 syl5ibrcom 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> ( C = B -> A <_ C ) )
48 40 44 47 3jaod 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> ( ( C = A \/ ( A < C /\ C < B ) \/ C = B ) -> A <_ C ) )
49 48 exp31 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. RR* -> ( A <_ B -> ( ( C = A \/ ( A < C /\ C < B ) \/ C = B ) -> A <_ C ) ) ) )
50 49 3impd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ B /\ ( C = A \/ ( A < C /\ C < B ) \/ C = B ) ) -> A <_ C ) )
51 breq1 
 |-  ( C = A -> ( C <_ B <-> A <_ B ) )
52 45 51 syl5ibrcom 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> ( C = A -> C <_ B ) )
53 xrltle 
 |-  ( ( C e. RR* /\ B e. RR* ) -> ( C < B -> C <_ B ) )
54 53 ancoms 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( C < B -> C <_ B ) )
55 54 adantld 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( ( A < C /\ C < B ) -> C <_ B ) )
56 55 adantll 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( ( A < C /\ C < B ) -> C <_ B ) )
57 56 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> ( ( A < C /\ C < B ) -> C <_ B ) )
58 xrleid 
 |-  ( B e. RR* -> B <_ B )
59 58 ad3antlr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> B <_ B )
60 breq1 
 |-  ( C = B -> ( C <_ B <-> B <_ B ) )
61 59 60 syl5ibrcom 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> ( C = B -> C <_ B ) )
62 52 57 61 3jaod 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ A <_ B ) -> ( ( C = A \/ ( A < C /\ C < B ) \/ C = B ) -> C <_ B ) )
63 62 exp31 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. RR* -> ( A <_ B -> ( ( C = A \/ ( A < C /\ C < B ) \/ C = B ) -> C <_ B ) ) ) )
64 63 3impd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ B /\ ( C = A \/ ( A < C /\ C < B ) \/ C = B ) ) -> C <_ B ) )
65 36 50 64 3jcad 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ B /\ ( C = A \/ ( A < C /\ C < B ) \/ C = B ) ) -> ( C e. RR* /\ A <_ C /\ C <_ B ) ) )
66 34 65 impbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ C /\ C <_ B ) <-> ( C e. RR* /\ A <_ B /\ ( C = A \/ ( A < C /\ C < B ) \/ C = B ) ) ) )
67 1 66 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ A <_ B /\ ( C = A \/ ( A < C /\ C < B ) \/ C = B ) ) ) )