This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem difico

Description: The difference between two closed-below, open-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 13-Oct-2017)

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

Proof

Step	Hyp	Ref	Expression
1		icodisj	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to [A, B) \cap [B, C) = \emptyset$
2		undif4	$⊢ [A, B) \cap [B, C) = \emptyset \to [A, B) \cup ([B, C) ∖ [B, C)) = ([A, B) \cup [B, C)) ∖ [B, C)$
3	1 2	syl	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to [A, B) \cup ([B, C) ∖ [B, C)) = ([A, B) \cup [B, C)) ∖ [B, C)$
4	3	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to [A, B) \cup ([B, C) ∖ [B, C)) = ([A, B) \cup [B, C)) ∖ [B, C)$
5		difid	$⊢ [B, C) ∖ [B, C) = \emptyset$
6	5	uneq2i	$⊢ [A, B) \cup ([B, C) ∖ [B, C)) = [A, B) \cup \emptyset$
7		un0	$⊢ [A, B) \cup \emptyset = [A, B)$
8	6 7	eqtri	$⊢ [A, B) \cup ([B, C) ∖ [B, C)) = [A, B)$
9	8	a1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to [A, B) \cup ([B, C) ∖ [B, C)) = [A, B)$
10		icoun	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to [A, B) \cup [B, C) = [A, C)$
11	10	difeq1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to ([A, B) \cup [B, C)) ∖ [B, C) = [A, C) ∖ [B, C)$
12	4 9 11	3eqtr3rd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to [A, C) ∖ [B, C) = [A, B)$