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∈AB→AB=AC∪CB

Proof

Step Hyp Ref Expression
1 simplr1 ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B∧x<C→x∈ℝ
2 simplr2 ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B∧x<C→A≤x
3 simpr1 ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B→x∈ℝ
4 iccssre ⊢A∈ℝ∧B∈ℝ→AB⊆ℝ
5 4 sseld ⊢A∈ℝ∧B∈ℝ→C∈AB→C∈ℝ
6 5 3impia ⊢A∈ℝ∧B∈ℝ∧C∈AB→C∈ℝ
7 6 adantr ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B→C∈ℝ
8 ltle ⊢x∈ℝ∧C∈ℝ→x<C→x≤C
9 3 7 8 syl2anc ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B→x<C→x≤C
10 9 imp ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B∧x<C→x≤C
11 1 2 10 3jca ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B∧x<C→x∈ℝ∧A≤x∧x≤C
12 11 orcd ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B∧x<C→x∈ℝ∧A≤x∧x≤C∨x∈ℝ∧C≤x∧x≤B
13 simplr1 ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B∧C≤x→x∈ℝ
14 simpr ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B∧C≤x→C≤x
15 simplr3 ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B∧C≤x→x≤B
16 13 14 15 3jca ⊢A∈ℝ∧B∈ℝ∧C∈AB∧x∈ℝ∧A≤x∧x≤B∧C≤x→x∈ℝ∧C≤x∧x≤B
17 16 olcd ⊢A∈ℝ∧B∈ℝ∧C∈AB∧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∈AB∧x∈ℝ∧A≤x∧x≤B→x∈ℝ∧A≤x∧x≤C∨x∈ℝ∧C≤x∧x≤B
19 18 ex ⊢A∈ℝ∧B∈ℝ∧C∈AB→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∈AB→x∈ℝ∧A≤x∧x≤C→x∈ℝ
22 simp2 ⊢x∈ℝ∧A≤x∧x≤C→A≤x
23 22 a1i ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈ℝ∧A≤x∧x≤C→A≤x
24 elicc2 ⊢A∈ℝ∧B∈ℝ→C∈AB↔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∈AB→x∈ℝ∧A≤x∧x≤C→x≤B
36 35 3impia ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈ℝ∧A≤x∧x≤C→x≤B
37 21 23 36 3jcad ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈ℝ∧A≤x∧x≤C→x∈ℝ∧A≤x∧x≤B
38 simp1 ⊢x∈ℝ∧C≤x∧x≤B→x∈ℝ
39 38 a1i ⊢A∈ℝ∧B∈ℝ∧C∈AB→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∈AB→x∈ℝ∧C≤x∧x≤B→A≤x
50 49 3impia ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈ℝ∧C≤x∧x≤B→A≤x
51 simp3 ⊢x∈ℝ∧C≤x∧x≤B→x≤B
52 51 a1i ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈ℝ∧C≤x∧x≤B→x≤B
53 39 50 52 3jcad ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈ℝ∧C≤x∧x≤B→x∈ℝ∧A≤x∧x≤B
54 37 53 jaod ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈ℝ∧A≤x∧x≤C∨x∈ℝ∧C≤x∧x≤B→x∈ℝ∧A≤x∧x≤B
55 19 54 impbid ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈ℝ∧A≤x∧x≤B↔x∈ℝ∧A≤x∧x≤C∨x∈ℝ∧C≤x∧x≤B
56 elicc2 ⊢A∈ℝ∧B∈ℝ→x∈AB↔x∈ℝ∧A≤x∧x≤B
57 56 3adant3 ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈AB↔x∈ℝ∧A≤x∧x≤B
58 5 imdistani ⊢A∈ℝ∧B∈ℝ∧C∈AB→A∈ℝ∧B∈ℝ∧C∈ℝ
59 58 3impa ⊢A∈ℝ∧B∈ℝ∧C∈AB→A∈ℝ∧B∈ℝ∧C∈ℝ
60 elicc2 ⊢A∈ℝ∧C∈ℝ→x∈AC↔x∈ℝ∧A≤x∧x≤C
61 60 adantlr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→x∈AC↔x∈ℝ∧A≤x∧x≤C
62 elicc2 ⊢C∈ℝ∧B∈ℝ→x∈CB↔x∈ℝ∧C≤x∧x≤B
63 62 ancoms ⊢B∈ℝ∧C∈ℝ→x∈CB↔x∈ℝ∧C≤x∧x≤B
64 63 adantll ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→x∈CB↔x∈ℝ∧C≤x∧x≤B
65 61 64 orbi12d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→x∈AC∨x∈CB↔x∈ℝ∧A≤x∧x≤C∨x∈ℝ∧C≤x∧x≤B
66 59 65 syl ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈AC∨x∈CB↔x∈ℝ∧A≤x∧x≤C∨x∈ℝ∧C≤x∧x≤B
67 55 57 66 3bitr4d ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈AB↔x∈AC∨x∈CB
68 elun ⊢x∈AC∪CB↔x∈AC∨x∈CB
69 67 68 bitr4di ⊢A∈ℝ∧B∈ℝ∧C∈AB→x∈AB↔x∈AC∪CB
70 69 eqrdv ⊢A∈ℝ∧B∈ℝ∧C∈AB→AB=AC∪CB