iccdificc

Description: The difference of two closed intervals with the same lower bound. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	iccdificc.a	$⊢ φ \to A \in ℝ^{*}$
	iccdificc.b	$⊢ φ \to B \in ℝ^{*}$
	iccdificc.c	$⊢ φ \to C \in ℝ^{*}$
	iccdificc.4	$⊢ φ \to A \leq B$
Assertion	iccdificc	$⊢ φ \to [A, C] ∖ [A, B] = (B, C]$

Proof

Step	Hyp	Ref	Expression
1		iccdificc.a	$⊢ φ \to A \in ℝ^{*}$
2		iccdificc.b	$⊢ φ \to B \in ℝ^{*}$
3		iccdificc.c	$⊢ φ \to C \in ℝ^{*}$
4		iccdificc.4	$⊢ φ \to A \leq B$
5	2	adantr	$⊢ (φ \land x \in ([A, C] ∖ [A, B])) \to B \in ℝ^{*}$
6	3	adantr	$⊢ (φ \land x \in ([A, C] ∖ [A, B])) \to C \in ℝ^{*}$
7		iccssxr	$⊢ [A, C] \subseteq ℝ^{*}$
8		eldifi	$⊢ x \in ([A, C] ∖ [A, B]) \to x \in [A, C]$
9	7 8	sselid	$⊢ x \in ([A, C] ∖ [A, B]) \to x \in ℝ^{*}$
10	9	adantl	$⊢ (φ \land x \in ([A, C] ∖ [A, B])) \to x \in ℝ^{*}$
11	1	ad2antrr	$⊢ ((φ \land x \in ([A, C] ∖ [A, B])) \land \neg B < x) \to A \in ℝ^{*}$
12	5	adantr	$⊢ ((φ \land x \in ([A, C] ∖ [A, B])) \land \neg B < x) \to B \in ℝ^{*}$
13	10	adantr	$⊢ ((φ \land x \in ([A, C] ∖ [A, B])) \land \neg B < x) \to x \in ℝ^{*}$
14	1	adantr	$⊢ (φ \land x \in ([A, C] ∖ [A, B])) \to A \in ℝ^{*}$
15	8	adantl	$⊢ (φ \land x \in ([A, C] ∖ [A, B])) \to x \in [A, C]$
16		iccgelb	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land x \in [A, C]) \to A \leq x$
17	14 6 15 16	syl3anc	$⊢ (φ \land x \in ([A, C] ∖ [A, B])) \to A \leq x$
18	17	adantr	$⊢ ((φ \land x \in ([A, C] ∖ [A, B])) \land \neg B < x) \to A \leq x$
19		simpr	$⊢ ((φ \land x \in ([A, C] ∖ [A, B])) \land \neg B < x) \to \neg B < x$
20	10 5	xrlenltd	$⊢ (φ \land x \in ([A, C] ∖ [A, B])) \to (x \leq B \leftrightarrow \neg B < x)$
21	20	adantr	$⊢ ((φ \land x \in ([A, C] ∖ [A, B])) \land \neg B < x) \to (x \leq B \leftrightarrow \neg B < x)$
22	19 21	mpbird	$⊢ ((φ \land x \in ([A, C] ∖ [A, B])) \land \neg B < x) \to x \leq B$
23	11 12 13 18 22	eliccxrd	$⊢ ((φ \land x \in ([A, C] ∖ [A, B])) \land \neg B < x) \to x \in [A, B]$
24		eldifn	$⊢ x \in ([A, C] ∖ [A, B]) \to \neg x \in [A, B]$
25	24	ad2antlr	$⊢ ((φ \land x \in ([A, C] ∖ [A, B])) \land \neg B < x) \to \neg x \in [A, B]$
26	23 25	condan	$⊢ (φ \land x \in ([A, C] ∖ [A, B])) \to B < x$
27		iccleub	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land x \in [A, C]) \to x \leq C$
28	14 6 15 27	syl3anc	$⊢ (φ \land x \in ([A, C] ∖ [A, B])) \to x \leq C$
29	5 6 10 26 28	eliocd	$⊢ (φ \land x \in ([A, C] ∖ [A, B])) \to x \in (B, C]$
30	29	ralrimiva	$⊢ φ \to \forall x \in ([A, C] ∖ [A, B]) x \in (B, C]$
31		dfss3	$⊢ [A, C] ∖ [A, B] \subseteq (B, C] \leftrightarrow \forall x \in ([A, C] ∖ [A, B]) x \in (B, C]$
32	30 31	sylibr	$⊢ φ \to [A, C] ∖ [A, B] \subseteq (B, C]$
33	1	adantr	$⊢ (φ \land x \in (B, C]) \to A \in ℝ^{*}$
34	3	adantr	$⊢ (φ \land x \in (B, C]) \to C \in ℝ^{*}$
35		iocssxr	$⊢ (B, C] \subseteq ℝ^{*}$
36		id	$⊢ x \in (B, C] \to x \in (B, C]$
37	35 36	sselid	$⊢ x \in (B, C] \to x \in ℝ^{*}$
38	37	adantl	$⊢ (φ \land x \in (B, C]) \to x \in ℝ^{*}$
39	2	adantr	$⊢ (φ \land x \in (B, C]) \to B \in ℝ^{*}$
40	4	adantr	$⊢ (φ \land x \in (B, C]) \to A \leq B$
41		simpr	$⊢ (φ \land x \in (B, C]) \to x \in (B, C]$
42		iocgtlb	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land x \in (B, C]) \to B < x$
43	39 34 41 42	syl3anc	$⊢ (φ \land x \in (B, C]) \to B < x$
44	33 39 38 40 43	xrlelttrd	$⊢ (φ \land x \in (B, C]) \to A < x$
45	33 38 44	xrltled	$⊢ (φ \land x \in (B, C]) \to A \leq x$
46		iocleub	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land x \in (B, C]) \to x \leq C$
47	39 34 41 46	syl3anc	$⊢ (φ \land x \in (B, C]) \to x \leq C$
48	33 34 38 45 47	eliccxrd	$⊢ (φ \land x \in (B, C]) \to x \in [A, C]$
49	33 39 38 43	xrgtnelicc	$⊢ (φ \land x \in (B, C]) \to \neg x \in [A, B]$
50	48 49	eldifd	$⊢ (φ \land x \in (B, C]) \to x \in ([A, C] ∖ [A, B])$
51	32 50	eqelssd	$⊢ φ \to [A, C] ∖ [A, B] = (B, C]$

Metamath Proof Explorer

Theorem iccdificc

Proof