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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) = ( ( 𝐴 [,] 𝐶 ) ∪ ( 𝐶 [,] 𝐵 ) ) )

Proof

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