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∈AB↔C∈ℝ*∧A≤B∧C=A∨A<C∧C<B∨C=B

Proof

Step Hyp Ref Expression
1 elicc1 ⊢A∈ℝ*∧B∈ℝ*→C∈AB↔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 biimtrrid ⊢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 biimtrid ⊢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 imbitrdi ⊢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∈AB↔C∈ℝ*∧A≤B∧C=A∨A<C∧C<B∨C=B