Metamath Proof Explorer

Theorem difioo

Description: The difference between two open intervals sharing the same lower bound. (Contributed by Thierry Arnoux, 26-Sep-2017)

Ref Expression
Assertion difioo ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐶 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 [,) 𝐶 ) )

Proof

Step Hyp Ref Expression
1 incom ⊢ ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ( ( 𝐵 [,) 𝐶 ) ∩ ( 𝐴 (,) 𝐵 ) )
2 joiniooico ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ ∧ ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) ) )
3 2 anassrs ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ ∧ ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) ) )
4 3 simpld ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ )
5 1 4 eqtr3id ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐵 [,) 𝐶 ) ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
6 3 simprd ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) )
7 uncom ⊢ ( ( 𝐵 [,) 𝐶 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) )
8 7 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐵 [,) 𝐶 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) )
9 simpll1 ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → 𝐴 ∈ ℝ* )
10 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐶 ∈ ℝ* )
11 10 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → 𝐶 ∈ ℝ* )
12 9 xrleidd ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → 𝐴 ≤ 𝐴 )
13 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → 𝐵 ≤ 𝐶 )
14 ioossioo ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐵 ≤ 𝐶 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐶 ) )
15 9 11 12 13 14 syl22anc ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐶 ) )
16 ssequn2 ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐶 ) ↔ ( ( 𝐴 (,) 𝐶 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐶 ) )
17 15 16 sylib ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 (,) 𝐶 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐶 ) )
18 6 8 17 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐵 [,) 𝐶 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝐴 (,) 𝐶 ) ∪ ( 𝐴 (,) 𝐵 ) ) )
19 difeq ⊢ ( ( ( 𝐴 (,) 𝐶 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 [,) 𝐶 ) ↔ ( ( ( 𝐵 [,) 𝐶 ) ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ∧ ( ( 𝐵 [,) 𝐶 ) ∪ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝐴 (,) 𝐶 ) ∪ ( 𝐴 (,) 𝐵 ) ) ) )
20 5 18 19 sylanbrc ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 (,) 𝐶 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 [,) 𝐶 ) )
21 simpll1 ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐵 ) → 𝐴 ∈ ℝ* )
22 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ* )
23 22 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐵 ) → 𝐵 ∈ ℝ* )
24 21 xrleidd ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐵 ) → 𝐴 ≤ 𝐴 )
25 10 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐵 ) → 𝐶 ∈ ℝ* )
26 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐵 ) → 𝐶 < 𝐵 )
27 25 23 26 xrltled ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐵 ) → 𝐶 ≤ 𝐵 )
28 ioossioo ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐶 ≤ 𝐵 ) ) → ( 𝐴 (,) 𝐶 ) ⊆ ( 𝐴 (,) 𝐵 ) )
29 21 23 24 27 28 syl22anc ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐵 ) → ( 𝐴 (,) 𝐶 ) ⊆ ( 𝐴 (,) 𝐵 ) )
30 ssdif0 ⊢ ( ( 𝐴 (,) 𝐶 ) ⊆ ( 𝐴 (,) 𝐵 ) ↔ ( ( 𝐴 (,) 𝐶 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ∅ )
31 29 30 sylib ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐵 ) → ( ( 𝐴 (,) 𝐶 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ∅ )
32 ico0 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐵 [,) 𝐶 ) = ∅ ↔ 𝐶 ≤ 𝐵 ) )
33 32 biimpar ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐶 ≤ 𝐵 ) → ( 𝐵 [,) 𝐶 ) = ∅ )
34 23 25 27 33 syl21anc ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐵 ) → ( 𝐵 [,) 𝐶 ) = ∅ )
35 31 34 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐵 ) → ( ( 𝐴 (,) 𝐶 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 [,) 𝐶 ) )
36 xrlelttric ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 ≤ 𝐶 ∨ 𝐶 < 𝐵 ) )
37 22 10 36 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 ≤ 𝐶 ∨ 𝐶 < 𝐵 ) )
38 20 35 37 mpjaodan ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐶 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 [,) 𝐶 ) )