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