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