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 e. RR /\ B e. RR /\ C e. ( A [,] B ) ) -> ( A [,] B ) = ( ( A [,] C ) u. ( C [,] B ) ) )

Proof

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