difreicc

Description: The class difference of RR and a closed interval. (Contributed by FL, 18-Jun-2007)

		Ref	Expression
	Assertion	difreicc	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ [A, B] = (−∞, A) \cup (B, +∞)$

Proof

Step	Hyp	Ref	Expression
1		eldif	$⊢ x \in (ℝ ∖ [A, B]) \leftrightarrow (x \in ℝ \land \neg x \in [A, B])$
2		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
3		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
4		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (x \in [A, B] \leftrightarrow (x \in ℝ^{*} \land A \leq x \land x \leq B))$
5	2 3 4	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in [A, B] \leftrightarrow (x \in ℝ^{*} \land A \leq x \land x \leq B))$
6	5	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (x \in [A, B] \leftrightarrow (x \in ℝ^{*} \land A \leq x \land x \leq B))$
7	6	notbid	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (\neg x \in [A, B] \leftrightarrow \neg (x \in ℝ^{*} \land A \leq x \land x \leq B))$
8		3anass	$⊢ (x \in ℝ^{} \land A \leq x \land x \leq B) \leftrightarrow (x \in ℝ^{} \land (A \leq x \land x \leq B))$
9	8	notbii	$⊢ \neg (x \in ℝ^{} \land A \leq x \land x \leq B) \leftrightarrow \neg (x \in ℝ^{} \land (A \leq x \land x \leq B))$
10		ianor	$⊢ \neg (x \in ℝ^{} \land (A \leq x \land x \leq B)) \leftrightarrow (\neg x \in ℝ^{} \lor \neg (A \leq x \land x \leq B))$
11		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
12	11	pm2.24d	$⊢ x \in ℝ \to (\neg x \in ℝ^{*} \to (x \in (−∞, A) \lor x \in (B, +∞)))$
13	12	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (\neg x \in ℝ^{*} \to (x \in (−∞, A) \lor x \in (B, +∞)))$
14		ianor	$⊢ \neg (A \leq x \land x \leq B) \leftrightarrow (\neg A \leq x \lor \neg x \leq B)$
15	11	ad2antlr	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land \neg A \leq x) \to x \in ℝ^{*}$
16		mnflt	$⊢ x \in ℝ \to −∞ < x$
17	16	ad2antlr	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land \neg A \leq x) \to −∞ < x$
18		simpr	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to x \in ℝ$
19		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to A \in ℝ$
20		ltnle	$⊢ (x \in ℝ \land A \in ℝ) \to (x < A \leftrightarrow \neg A \leq x)$
21	20	bicomd	$⊢ (x \in ℝ \land A \in ℝ) \to (\neg A \leq x \leftrightarrow x < A)$
22	18 19 21	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (\neg A \leq x \leftrightarrow x < A)$
23	22	biimpa	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land \neg A \leq x) \to x < A$
24		mnfxr	$⊢ −∞ \in ℝ^{*}$
25	2	ad3antrrr	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land \neg A \leq x) \to A \in ℝ^{*}$
26		elioo1	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{}) \to (x \in (−∞, A) \leftrightarrow (x \in ℝ^{*} \land −∞ < x \land x < A))$
27	24 25 26	sylancr	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land \neg A \leq x) \to (x \in (−∞, A) \leftrightarrow (x \in ℝ^{*} \land −∞ < x \land x < A))$
28	15 17 23 27	mpbir3and	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land \neg A \leq x) \to x \in (−∞, A)$
29	28	ex	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (\neg A \leq x \to x \in (−∞, A))$
30		ltnle	$⊢ (B \in ℝ \land x \in ℝ) \to (B < x \leftrightarrow \neg x \leq B)$
31	30	adantll	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (B < x \leftrightarrow \neg x \leq B)$
32	11	ad2antlr	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land B < x) \to x \in ℝ^{*}$
33		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land B < x) \to B < x$
34		ltpnf	$⊢ x \in ℝ \to x < +∞$
35	34	ad2antlr	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land B < x) \to x < +∞$
36	3	ad3antlr	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land B < x) \to B \in ℝ^{*}$
37		pnfxr	$⊢ +∞ \in ℝ^{*}$
38		elioo1	$⊢ (B \in ℝ^{} \land +∞ \in ℝ^{}) \to (x \in (B, +∞) \leftrightarrow (x \in ℝ^{*} \land B < x \land x < +∞))$
39	36 37 38	sylancl	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land B < x) \to (x \in (B, +∞) \leftrightarrow (x \in ℝ^{*} \land B < x \land x < +∞))$
40	32 33 35 39	mpbir3and	$⊢ (((A \in ℝ \land B \in ℝ) \land x \in ℝ) \land B < x) \to x \in (B, +∞)$
41	40	ex	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (B < x \to x \in (B, +∞))$
42	31 41	sylbird	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (\neg x \leq B \to x \in (B, +∞))$
43	29 42	orim12d	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to ((\neg A \leq x \lor \neg x \leq B) \to (x \in (−∞, A) \lor x \in (B, +∞)))$
44	14 43	syl5bi	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (\neg (A \leq x \land x \leq B) \to (x \in (−∞, A) \lor x \in (B, +∞)))$
45	13 44	jaod	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to ((\neg x \in ℝ^{*} \lor \neg (A \leq x \land x \leq B)) \to (x \in (−∞, A) \lor x \in (B, +∞)))$
46	10 45	syl5bi	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (\neg (x \in ℝ^{*} \land (A \leq x \land x \leq B)) \to (x \in (−∞, A) \lor x \in (B, +∞)))$
47	9 46	syl5bi	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (\neg (x \in ℝ^{*} \land A \leq x \land x \leq B) \to (x \in (−∞, A) \lor x \in (B, +∞)))$
48	7 47	sylbid	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ℝ) \to (\neg x \in [A, B] \to (x \in (−∞, A) \lor x \in (B, +∞)))$
49	48	expimpd	$⊢ (A \in ℝ \land B \in ℝ) \to ((x \in ℝ \land \neg x \in [A, B]) \to (x \in (−∞, A) \lor x \in (B, +∞)))$
50		elun	$⊢ x \in ((−∞, A) \cup (B, +∞)) \leftrightarrow (x \in (−∞, A) \lor x \in (B, +∞))$
51	49 50	syl6ibr	$⊢ (A \in ℝ \land B \in ℝ) \to ((x \in ℝ \land \neg x \in [A, B]) \to x \in ((−∞, A) \cup (B, +∞)))$
52		ioossre	$⊢ (−∞, A) \subseteq ℝ$
53		ioossre	$⊢ (B, +∞) \subseteq ℝ$
54	52 53	unssi	$⊢ (−∞, A) \cup (B, +∞) \subseteq ℝ$
55	54	sseli	$⊢ x \in ((−∞, A) \cup (B, +∞)) \to x \in ℝ$
56	55	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ((−∞, A) \cup (B, +∞))) \to x \in ℝ$
57		elioo2	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{}) \to (x \in (−∞, A) \leftrightarrow (x \in ℝ \land −∞ < x \land x < A))$
58	24 2 57	sylancr	$⊢ A \in ℝ \to (x \in (−∞, A) \leftrightarrow (x \in ℝ \land −∞ < x \land x < A))$
59	58	adantr	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in (−∞, A) \leftrightarrow (x \in ℝ \land −∞ < x \land x < A))$
60	20	biimpd	$⊢ (x \in ℝ \land A \in ℝ) \to (x < A \to \neg A \leq x)$
61	60	ex	$⊢ x \in ℝ \to (A \in ℝ \to (x < A \to \neg A \leq x))$
62	61	a1i	$⊢ −∞ < x \to (x \in ℝ \to (A \in ℝ \to (x < A \to \neg A \leq x)))$
63	62	com13	$⊢ A \in ℝ \to (x \in ℝ \to (−∞ < x \to (x < A \to \neg A \leq x)))$
64	63	adantr	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in ℝ \to (−∞ < x \to (x < A \to \neg A \leq x)))$
65	64	3impd	$⊢ (A \in ℝ \land B \in ℝ) \to ((x \in ℝ \land −∞ < x \land x < A) \to \neg A \leq x)$
66	59 65	sylbid	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in (−∞, A) \to \neg A \leq x)$
67	3	adantl	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ^{*}$
68	67 37 38	sylancl	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in (B, +∞) \leftrightarrow (x \in ℝ^{*} \land B < x \land x < +∞))$
69		xrltnle	$⊢ (B \in ℝ^{} \land x \in ℝ^{}) \to (B < x \leftrightarrow \neg x \leq B)$
70	69	biimpd	$⊢ (B \in ℝ^{} \land x \in ℝ^{}) \to (B < x \to \neg x \leq B)$
71	70	ex	$⊢ B \in ℝ^{} \to (x \in ℝ^{} \to (B < x \to \neg x \leq B))$
72	71	a1ddd	$⊢ B \in ℝ^{} \to (x \in ℝ^{} \to (B < x \to (x < +∞ \to \neg x \leq B)))$
73	3 72	syl	$⊢ B \in ℝ \to (x \in ℝ^{*} \to (B < x \to (x < +∞ \to \neg x \leq B)))$
74	73	adantl	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in ℝ^{*} \to (B < x \to (x < +∞ \to \neg x \leq B)))$
75	74	3impd	$⊢ (A \in ℝ \land B \in ℝ) \to ((x \in ℝ^{*} \land B < x \land x < +∞) \to \neg x \leq B)$
76	68 75	sylbid	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in (B, +∞) \to \neg x \leq B)$
77	66 76	orim12d	$⊢ (A \in ℝ \land B \in ℝ) \to ((x \in (−∞, A) \lor x \in (B, +∞)) \to (\neg A \leq x \lor \neg x \leq B))$
78	50 77	syl5bi	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in ((−∞, A) \cup (B, +∞)) \to (\neg A \leq x \lor \neg x \leq B))$
79	78	imp	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ((−∞, A) \cup (B, +∞))) \to (\neg A \leq x \lor \neg x \leq B)$
80	79 14	sylibr	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ((−∞, A) \cup (B, +∞))) \to \neg (A \leq x \land x \leq B)$
81	80	intnand	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ((−∞, A) \cup (B, +∞))) \to \neg (x \in ℝ^{*} \land (A \leq x \land x \leq B))$
82	81 8	sylnibr	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ((−∞, A) \cup (B, +∞))) \to \neg (x \in ℝ^{*} \land A \leq x \land x \leq B)$
83	2 3	anim12i	$⊢ (A \in ℝ \land B \in ℝ) \to (A \in ℝ^{} \land B \in ℝ^{})$
84	83	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ((−∞, A) \cup (B, +∞))) \to (A \in ℝ^{} \land B \in ℝ^{})$
85	4	notbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg x \in [A, B] \leftrightarrow \neg (x \in ℝ^{*} \land A \leq x \land x \leq B))$
86	84 85	syl	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ((−∞, A) \cup (B, +∞))) \to (\neg x \in [A, B] \leftrightarrow \neg (x \in ℝ^{*} \land A \leq x \land x \leq B))$
87	82 86	mpbird	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ((−∞, A) \cup (B, +∞))) \to \neg x \in [A, B]$
88	56 87	jca	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in ((−∞, A) \cup (B, +∞))) \to (x \in ℝ \land \neg x \in [A, B])$
89	88	ex	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in ((−∞, A) \cup (B, +∞)) \to (x \in ℝ \land \neg x \in [A, B]))$
90	51 89	impbid	$⊢ (A \in ℝ \land B \in ℝ) \to ((x \in ℝ \land \neg x \in [A, B]) \leftrightarrow x \in ((−∞, A) \cup (B, +∞)))$
91	1 90	syl5bb	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in (ℝ ∖ [A, B]) \leftrightarrow x \in ((−∞, A) \cup (B, +∞)))$
92	91	eqrdv	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ [A, B] = (−∞, A) \cup (B, +∞)$

Metamath Proof Explorer

Theorem difreicc

Proof