Theorem xrdifh

Description: Class difference of a half-open interval in the extended reals. (Contributed by Thierry Arnoux, 1-Aug-2017)

	Ref	Expression
Hypothesis	xrdifh.1	$$⊢A\in {ℝ}^{*}$$
Assertion	xrdifh	$$⊢{ℝ}^{*}\setminus \left[A,\mathrm{+\infty }\right]=\left[\mathrm{-\infty },A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrdifh.1	$$⊢A\in {ℝ}^{*}$$
2		biortn	$$⊢x\in {ℝ}^{*}\to \left(\left(\neg A\le x\vee \neg x\le \mathrm{+\infty }\right)\leftrightarrow \left(\neg x\in {ℝ}^{*}\vee \left(\neg A\le x\vee \neg x\le \mathrm{+\infty }\right)\right)\right)$$
3		pnfge	$$⊢x\in {ℝ}^{*}\to x\le \mathrm{+\infty }$$
4	3	notnotd	$$⊢x\in {ℝ}^{*}\to \neg \neg x\le \mathrm{+\infty }$$
5		biorf	$$⊢\neg \neg x\le \mathrm{+\infty }\to \left(\neg A\le x\leftrightarrow \left(\neg x\le \mathrm{+\infty }\vee \neg A\le x\right)\right)$$
6	4 5	syl	$$⊢x\in {ℝ}^{*}\to \left(\neg A\le x\leftrightarrow \left(\neg x\le \mathrm{+\infty }\vee \neg A\le x\right)\right)$$
7		orcom	$$⊢\left(\neg A\le x\vee \neg x\le \mathrm{+\infty }\right)\leftrightarrow \left(\neg x\le \mathrm{+\infty }\vee \neg A\le x\right)$$
8	6 7	bitr4di	$$⊢x\in {ℝ}^{*}\to \left(\neg A\le x\leftrightarrow \left(\neg A\le x\vee \neg x\le \mathrm{+\infty }\right)\right)$$
9		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
10		elicc1	$$⊢\left(A\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(x\in \left[A,\mathrm{+\infty }\right]\leftrightarrow \left(x\in {ℝ}^{*}\wedge A\le x\wedge x\le \mathrm{+\infty }\right)\right)$$
11	1 9 10	mp2an	$$⊢x\in \left[A,\mathrm{+\infty }\right]\leftrightarrow \left(x\in {ℝ}^{*}\wedge A\le x\wedge x\le \mathrm{+\infty }\right)$$
12	11	notbii	$$⊢\neg x\in \left[A,\mathrm{+\infty }\right]\leftrightarrow \neg \left(x\in {ℝ}^{*}\wedge A\le x\wedge x\le \mathrm{+\infty }\right)$$
13		3ianor	$$⊢\neg \left(x\in {ℝ}^{*}\wedge A\le x\wedge x\le \mathrm{+\infty }\right)\leftrightarrow \left(\neg x\in {ℝ}^{*}\vee \neg A\le x\vee \neg x\le \mathrm{+\infty }\right)$$
14		3orass	$$⊢\left(\neg x\in {ℝ}^{*}\vee \neg A\le x\vee \neg x\le \mathrm{+\infty }\right)\leftrightarrow \left(\neg x\in {ℝ}^{*}\vee \left(\neg A\le x\vee \neg x\le \mathrm{+\infty }\right)\right)$$
15	12 13 14	3bitri	$$⊢\neg x\in \left[A,\mathrm{+\infty }\right]\leftrightarrow \left(\neg x\in {ℝ}^{*}\vee \left(\neg A\le x\vee \neg x\le \mathrm{+\infty }\right)\right)$$
16	15	a1i	$$⊢x\in {ℝ}^{*}\to \left(\neg x\in \left[A,\mathrm{+\infty }\right]\leftrightarrow \left(\neg x\in {ℝ}^{*}\vee \left(\neg A\le x\vee \neg x\le \mathrm{+\infty }\right)\right)\right)$$
17	2 8 16	3bitr4rd	$$⊢x\in {ℝ}^{*}\to \left(\neg x\in \left[A,\mathrm{+\infty }\right]\leftrightarrow \neg A\le x\right)$$
18		xrltnle	$$⊢\left(x\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(x<A\leftrightarrow \neg A\le x\right)$$
19	1 18	mpan2	$$⊢x\in {ℝ}^{*}\to \left(x<A\leftrightarrow \neg A\le x\right)$$
20	17 19	bitr4d	$$⊢x\in {ℝ}^{*}\to \left(\neg x\in \left[A,\mathrm{+\infty }\right]\leftrightarrow x<A\right)$$
21	20	pm5.32i	$$⊢\left(x\in {ℝ}^{*}\wedge \neg x\in \left[A,\mathrm{+\infty }\right]\right)\leftrightarrow \left(x\in {ℝ}^{*}\wedge x<A\right)$$
22		eldif	$$⊢x\in \left({ℝ}^{*}\setminus \left[A,\mathrm{+\infty }\right]\right)\leftrightarrow \left(x\in {ℝ}^{*}\wedge \neg x\in \left[A,\mathrm{+\infty }\right]\right)$$
23		3anass	$$⊢\left(x\in {ℝ}^{*}\wedge \mathrm{-\infty }\le x\wedge x<A\right)\leftrightarrow \left(x\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }\le x\wedge x<A\right)\right)$$
24		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
25		elico1	$$⊢\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(x\in \left[\mathrm{-\infty },A\right)\leftrightarrow \left(x\in {ℝ}^{*}\wedge \mathrm{-\infty }\le x\wedge x<A\right)\right)$$
26	24 1 25	mp2an	$$⊢x\in \left[\mathrm{-\infty },A\right)\leftrightarrow \left(x\in {ℝ}^{*}\wedge \mathrm{-\infty }\le x\wedge x<A\right)$$
27		mnfle	$$⊢x\in {ℝ}^{*}\to \mathrm{-\infty }\le x$$
28	27	biantrurd	$$⊢x\in {ℝ}^{*}\to \left(x<A\leftrightarrow \left(\mathrm{-\infty }\le x\wedge x<A\right)\right)$$
29	28	pm5.32i	$$⊢\left(x\in {ℝ}^{*}\wedge x<A\right)\leftrightarrow \left(x\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }\le x\wedge x<A\right)\right)$$
30	23 26 29	3bitr4i	$$⊢x\in \left[\mathrm{-\infty },A\right)\leftrightarrow \left(x\in {ℝ}^{*}\wedge x<A\right)$$
31	21 22 30	3bitr4i	$$⊢x\in \left({ℝ}^{*}\setminus \left[A,\mathrm{+\infty }\right]\right)\leftrightarrow x\in \left[\mathrm{-\infty },A\right)$$
32	31	eqriv	$$⊢{ℝ}^{*}\setminus \left[A,\mathrm{+\infty }\right]=\left[\mathrm{-\infty },A\right)$$