Metamath Proof Explorer

Theorem iccsplit

Description: Split a closed interval into the union of two closed intervals. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion iccsplit ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → A B = A C ∪ C B

Proof

Step Hyp Ref Expression
1 simplr1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ∧ x < C → x ∈ ℝ
2 simplr2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ∧ x < C → A ≤ x
3 simpr1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B → x ∈ ℝ
4 iccssre ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ⊆ ℝ
5 4 sseld ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ A B → C ∈ ℝ
6 5 3impia ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → C ∈ ℝ
7 6 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B → C ∈ ℝ
8 ltle ⊢ x ∈ ℝ ∧ C ∈ ℝ → x < C → x ≤ C
9 3 7 8 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B → x < C → x ≤ C
10 9 imp ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ∧ x < C → x ≤ C
11 1 2 10 3jca ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ∧ x < C → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C
12 11 orcd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ∧ x < C → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C ∨ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
13 simplr1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ∧ C ≤ x → x ∈ ℝ
14 simpr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ∧ C ≤ x → C ≤ x
15 simplr3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ∧ C ≤ x → x ≤ B
16 13 14 15 3jca ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ∧ C ≤ x → x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
17 16 olcd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ∧ C ≤ x → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C ∨ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
18 12 17 3 7 ltlecasei ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C ∨ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
19 18 ex ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C ∨ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
20 simp1 ⊢ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → x ∈ ℝ
21 20 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → x ∈ ℝ
22 simp2 ⊢ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → A ≤ x
23 22 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → A ≤ x
24 elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ A B ↔ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B
25 20 3ad2ant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → x ∈ ℝ
26 simp1 ⊢ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B → C ∈ ℝ
27 26 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → C ∈ ℝ
28 simp1r ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → B ∈ ℝ
29 simp3 ⊢ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → x ≤ C
30 29 3ad2ant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → x ≤ C
31 simp3 ⊢ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B → C ≤ B
32 31 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → C ≤ B
33 25 27 28 30 32 letrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → x ≤ B
34 33 3exp ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ ℝ ∧ A ≤ C ∧ C ≤ B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → x ≤ B
35 24 34 sylbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ A B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → x ≤ B
36 35 3impia ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → x ≤ B
37 21 23 36 3jcad ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C → x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
38 simp1 ⊢ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → x ∈ ℝ
39 38 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → x ∈ ℝ
40 simp1l ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → A ∈ ℝ
41 26 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → C ∈ ℝ
42 38 3ad2ant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → x ∈ ℝ
43 simp2 ⊢ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B → A ≤ C
44 43 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → A ≤ C
45 simp2 ⊢ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → C ≤ x
46 45 3ad2ant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → C ≤ x
47 40 41 42 44 46 letrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B ∧ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → A ≤ x
48 47 3exp ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ ℝ ∧ A ≤ C ∧ C ≤ B → x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → A ≤ x
49 24 48 sylbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ A B → x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → A ≤ x
50 49 3impia ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → A ≤ x
51 simp3 ⊢ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → x ≤ B
52 51 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → x ≤ B
53 39 50 52 3jcad ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
54 37 53 jaod ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ C ∨ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
55 19 54 impbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C ∨ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
56 elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → x ∈ A B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
57 56 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ A B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
58 5 imdistani ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ
59 58 3impa ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ
60 elicc2 ⊢ A ∈ ℝ ∧ C ∈ ℝ → x ∈ A C ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C
61 60 adantlr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → x ∈ A C ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C
62 elicc2 ⊢ C ∈ ℝ ∧ B ∈ ℝ → x ∈ C B ↔ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
63 62 ancoms ⊢ B ∈ ℝ ∧ C ∈ ℝ → x ∈ C B ↔ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
64 63 adantll ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → x ∈ C B ↔ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
65 61 64 orbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → x ∈ A C ∨ x ∈ C B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C ∨ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
66 59 65 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ A C ∨ x ∈ C B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ C ∨ x ∈ ℝ ∧ C ≤ x ∧ x ≤ B
67 55 57 66 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ A B ↔ x ∈ A C ∨ x ∈ C B
68 elun ⊢ x ∈ A C ∪ C B ↔ x ∈ A C ∨ x ∈ C B
69 67 68 bitr4di ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → x ∈ A B ↔ x ∈ A C ∪ C B
70 69 eqrdv ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → A B = A C ∪ C B