# 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 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\to \left({A},{C}\right)\setminus \left({A},{B}\right)=\left[{B},{C}\right)$

### Proof

Step Hyp Ref Expression
1 incom ${⊢}\left({A},{B}\right)\cap \left[{B},{C}\right)=\left[{B},{C}\right)\cap \left({A},{B}\right)$
2 joiniooico ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}<{B}\wedge {B}\le {C}\right)\right)\to \left(\left({A},{B}\right)\cap \left[{B},{C}\right)=\varnothing \wedge \left({A},{B}\right)\cup \left[{B},{C}\right)=\left({A},{C}\right)\right)$
3 2 anassrs ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to \left(\left({A},{B}\right)\cap \left[{B},{C}\right)=\varnothing \wedge \left({A},{B}\right)\cup \left[{B},{C}\right)=\left({A},{C}\right)\right)$
4 3 simpld ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to \left({A},{B}\right)\cap \left[{B},{C}\right)=\varnothing$
5 1 4 syl5eqr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to \left[{B},{C}\right)\cap \left({A},{B}\right)=\varnothing$
6 3 simprd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to \left({A},{B}\right)\cup \left[{B},{C}\right)=\left({A},{C}\right)$
7 uncom ${⊢}\left[{B},{C}\right)\cup \left({A},{B}\right)=\left({A},{B}\right)\cup \left[{B},{C}\right)$
8 7 a1i ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to \left[{B},{C}\right)\cup \left({A},{B}\right)=\left({A},{B}\right)\cup \left[{B},{C}\right)$
9 simpll1 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to {A}\in {ℝ}^{*}$
10 simpl3 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\to {C}\in {ℝ}^{*}$
11 10 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to {C}\in {ℝ}^{*}$
12 9 xrleidd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to {A}\le {A}$
13 simpr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to {B}\le {C}$
14 ioossioo ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}\le {A}\wedge {B}\le {C}\right)\right)\to \left({A},{B}\right)\subseteq \left({A},{C}\right)$
15 9 11 12 13 14 syl22anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to \left({A},{B}\right)\subseteq \left({A},{C}\right)$
16 ssequn2 ${⊢}\left({A},{B}\right)\subseteq \left({A},{C}\right)↔\left({A},{C}\right)\cup \left({A},{B}\right)=\left({A},{C}\right)$
17 15 16 sylib ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to \left({A},{C}\right)\cup \left({A},{B}\right)=\left({A},{C}\right)$
18 6 8 17 3eqtr4d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to \left[{B},{C}\right)\cup \left({A},{B}\right)=\left({A},{C}\right)\cup \left({A},{B}\right)$
19 difeq ${⊢}\left({A},{C}\right)\setminus \left({A},{B}\right)=\left[{B},{C}\right)↔\left(\left[{B},{C}\right)\cap \left({A},{B}\right)=\varnothing \wedge \left[{B},{C}\right)\cup \left({A},{B}\right)=\left({A},{C}\right)\cup \left({A},{B}\right)\right)$
20 5 18 19 sylanbrc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {B}\le {C}\right)\to \left({A},{C}\right)\setminus \left({A},{B}\right)=\left[{B},{C}\right)$
21 simpll1 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {C}<{B}\right)\to {A}\in {ℝ}^{*}$
22 simpl2 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\to {B}\in {ℝ}^{*}$
23 22 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {C}<{B}\right)\to {B}\in {ℝ}^{*}$
24 21 xrleidd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {C}<{B}\right)\to {A}\le {A}$
25 10 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {C}<{B}\right)\to {C}\in {ℝ}^{*}$
26 simpr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {C}<{B}\right)\to {C}<{B}$
27 25 23 26 xrltled ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {C}<{B}\right)\to {C}\le {B}$
28 ioossioo ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}\le {A}\wedge {C}\le {B}\right)\right)\to \left({A},{C}\right)\subseteq \left({A},{B}\right)$
29 21 23 24 27 28 syl22anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {C}<{B}\right)\to \left({A},{C}\right)\subseteq \left({A},{B}\right)$
30 ssdif0 ${⊢}\left({A},{C}\right)\subseteq \left({A},{B}\right)↔\left({A},{C}\right)\setminus \left({A},{B}\right)=\varnothing$
31 29 30 sylib ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {C}<{B}\right)\to \left({A},{C}\right)\setminus \left({A},{B}\right)=\varnothing$
32 ico0 ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left[{B},{C}\right)=\varnothing ↔{C}\le {B}\right)$
33 32 biimpar ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {C}\le {B}\right)\to \left[{B},{C}\right)=\varnothing$
34 23 25 27 33 syl21anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {C}<{B}\right)\to \left[{B},{C}\right)=\varnothing$
35 31 34 eqtr4d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\wedge {C}<{B}\right)\to \left({A},{C}\right)\setminus \left({A},{B}\right)=\left[{B},{C}\right)$
36 xrlelttric ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({B}\le {C}\vee {C}<{B}\right)$
37 22 10 36 syl2anc ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\to \left({B}\le {C}\vee {C}<{B}\right)$
38 20 35 37 mpjaodan ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}<{B}\right)\to \left({A},{C}\right)\setminus \left({A},{B}\right)=\left[{B},{C}\right)$