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 * B * C A B C * A B C = A A < C C < B C = B

Proof

Step Hyp Ref Expression
1 elicc1 A * B * C A B C * A C C B
2 simp1 C * A C C B C *
3 2 a1i A * B * C * A C C B C *
4 xrletr A * C * B * A C C B A B
5 4 exp5o A * C * B * A C C B A B
6 5 com23 A * B * C * A C C B A B
7 6 imp5q A * B * C * A C C B A B
8 df-ne C A ¬ C = A
9 xrleltne A * C * A C A < C C A
10 9 biimprd A * C * A C C A A < C
11 8 10 syl5bir A * C * A C ¬ C = A A < C
12 11 3adant3r3 A * C * A C C B ¬ C = A A < C
13 12 adantlr A * B * C * A C C B ¬ C = A A < C
14 eqcom C = B B = C
15 14 necon3bbii ¬ C = B B C
16 xrleltne C * B * C B C < B B C
17 16 biimprd C * B * C B B C C < B
18 15 17 syl5bi C * B * C B ¬ C = B C < B
19 18 3exp C * B * C B ¬ C = B C < B
20 19 com12 B * C * C B ¬ C = B C < B
21 20 imp32 B * C * C B ¬ C = B C < B
22 21 3adantr2 B * C * A C C B ¬ C = B C < B
23 22 adantll A * B * C * A C C B ¬ C = B C < B
24 13 23 anim12d A * B * C * A C C B ¬ C = A ¬ C = B A < C C < B
25 24 ex A * B * C * 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 * B * C * A C C B C = A A < C C < B C = B
34 3 7 33 3jcad A * B * C * A C C B C * A B C = A A < C C < B C = B
35 simp1 C * A B C = A A < C C < B C = B C *
36 35 a1i A * B * C * A B C = A A < C C < B C = B C *
37 xrleid A * A A
38 37 ad3antrrr A * B * C * A B A A
39 breq2 C = A A C A A
40 38 39 syl5ibrcom A * B * C * A B C = A A C
41 xrltle A * C * A < C A C
42 41 adantr A * C * A B A < C A C
43 42 adantllr A * B * C * A B A < C A C
44 43 adantrd A * B * C * A B A < C C < B A C
45 simpr A * B * C * A B A B
46 breq2 C = B A C A B
47 45 46 syl5ibrcom A * B * C * A B C = B A C
48 40 44 47 3jaod A * B * C * A B C = A A < C C < B C = B A C
49 48 exp31 A * B * C * A B C = A A < C C < B C = B A C
50 49 3impd A * B * C * 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 * B * C * A B C = A C B
53 xrltle C * B * C < B C B
54 53 ancoms B * C * C < B C B
55 54 adantld B * C * A < C C < B C B
56 55 adantll A * B * C * A < C C < B C B
57 56 adantr A * B * C * A B A < C C < B C B
58 xrleid B * B B
59 58 ad3antlr A * B * C * A B B B
60 breq1 C = B C B B B
61 59 60 syl5ibrcom A * B * C * A B C = B C B
62 52 57 61 3jaod A * B * C * A B C = A A < C C < B C = B C B
63 62 exp31 A * B * C * A B C = A A < C C < B C = B C B
64 63 3impd A * B * C * A B C = A A < C C < B C = B C B
65 36 50 64 3jcad A * B * C * A B C = A A < C C < B C = B C * A C C B
66 34 65 impbid A * B * C * A C C B C * A B C = A A < C C < B C = B
67 1 66 bitrd A * B * C A B C * A B C = A A < C C < B C = B