difioo

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

		Ref	Expression
	Assertion	difioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A < B) \to (A, C) ∖ (A, B) = [B, C)$

Proof

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

Metamath Proof Explorer

Theorem difioo

Proof