recld2

Description: The real numbers are a closed set in the topology on CC . (Contributed by Mario Carneiro, 17-Feb-2015)

		Ref	Expression
	Hypothesis	recld2.1	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	recld2	$⊢ ℝ \in Clsd (J)$

Proof

Step	Hyp	Ref	Expression
1		recld2.1	$⊢ J = TopOpen (ℂ_{fld})$
2		difss	$⊢ ℂ ∖ ℝ \subseteq ℂ$
3		eldifi	$⊢ x \in (ℂ ∖ ℝ) \to x \in ℂ$
4	3	imcld	$⊢ x \in (ℂ ∖ ℝ) \to ℑ (x) \in ℝ$
5	4	recnd	$⊢ x \in (ℂ ∖ ℝ) \to ℑ (x) \in ℂ$
6		eldifn	$⊢ x \in (ℂ ∖ ℝ) \to \neg x \in ℝ$
7		reim0b	$⊢ x \in ℂ \to (x \in ℝ \leftrightarrow ℑ (x) = 0)$
8	3 7	syl	$⊢ x \in (ℂ ∖ ℝ) \to (x \in ℝ \leftrightarrow ℑ (x) = 0)$
9	8	necon3bbid	$⊢ x \in (ℂ ∖ ℝ) \to (\neg x \in ℝ \leftrightarrow ℑ (x) \neq 0)$
10	6 9	mpbid	$⊢ x \in (ℂ ∖ ℝ) \to ℑ (x) \neq 0$
11	5 10	absrpcld	$⊢ x \in (ℂ ∖ ℝ) \to \|ℑ (x)\| \in ℝ^{+}$
12		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
13	5	abscld	$⊢ x \in (ℂ ∖ ℝ) \to \|ℑ (x)\| \in ℝ$
14	13	rexrd	$⊢ x \in (ℂ ∖ ℝ) \to \|ℑ (x)\| \in ℝ^{*}$
15		elbl	$⊢ (abs \circ - \in ∞Met (ℂ) \land x \in ℂ \land \|ℑ (x)\| \in ℝ^{*}) \to (y \in (x ball (abs \circ -) \|ℑ (x)\|) \leftrightarrow (y \in ℂ \land x (abs \circ -) y < \|ℑ (x)\|))$
16	12 3 14 15	mp3an2i	$⊢ x \in (ℂ ∖ ℝ) \to (y \in (x ball (abs \circ -) \|ℑ (x)\|) \leftrightarrow (y \in ℂ \land x (abs \circ -) y < \|ℑ (x)\|))$
17		simprl	$⊢ (x \in (ℂ ∖ ℝ) \land (y \in ℂ \land x (abs \circ -) y < \|ℑ (x)\|)) \to y \in ℂ$
18	3	adantr	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to x \in ℂ$
19		simpr	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to y \in ℝ$
20	19	recnd	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to y \in ℂ$
21		eqid	$⊢ abs \circ - = abs \circ -$
22	21	cnmetdval	$⊢ (x \in ℂ \land y \in ℂ) \to x (abs \circ -) y = \|x - y\|$
23	18 20 22	syl2anc	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to x (abs \circ -) y = \|x - y\|$
24	5	adantr	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to ℑ (x) \in ℂ$
25	24	abscld	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to \|ℑ (x)\| \in ℝ$
26	18 20	subcld	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to x - y \in ℂ$
27	26	abscld	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to \|x - y\| \in ℝ$
28	18 20	imsubd	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to ℑ (x - y) = ℑ (x) - ℑ (y)$
29		reim0	$⊢ y \in ℝ \to ℑ (y) = 0$
30	29	adantl	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to ℑ (y) = 0$
31	30	oveq2d	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to ℑ (x) - ℑ (y) = ℑ (x) - 0$
32	24	subid1d	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to ℑ (x) - 0 = ℑ (x)$
33	28 31 32	3eqtrd	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to ℑ (x - y) = ℑ (x)$
34	33	fveq2d	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to \|ℑ (x - y)\| = \|ℑ (x)\|$
35		absimle	$⊢ x - y \in ℂ \to \|ℑ (x - y)\| \leq \|x - y\|$
36	26 35	syl	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to \|ℑ (x - y)\| \leq \|x - y\|$
37	34 36	eqbrtrrd	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to \|ℑ (x)\| \leq \|x - y\|$
38	25 27 37	lensymd	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to \neg \|x - y\| < \|ℑ (x)\|$
39	23 38	eqnbrtrd	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℝ) \to \neg x (abs \circ -) y < \|ℑ (x)\|$
40	39	ex	$⊢ x \in (ℂ ∖ ℝ) \to (y \in ℝ \to \neg x (abs \circ -) y < \|ℑ (x)\|)$
41	40	con2d	$⊢ x \in (ℂ ∖ ℝ) \to (x (abs \circ -) y < \|ℑ (x)\| \to \neg y \in ℝ)$
42	41	adantr	$⊢ (x \in (ℂ ∖ ℝ) \land y \in ℂ) \to (x (abs \circ -) y < \|ℑ (x)\| \to \neg y \in ℝ)$
43	42	impr	$⊢ (x \in (ℂ ∖ ℝ) \land (y \in ℂ \land x (abs \circ -) y < \|ℑ (x)\|)) \to \neg y \in ℝ$
44	17 43	eldifd	$⊢ (x \in (ℂ ∖ ℝ) \land (y \in ℂ \land x (abs \circ -) y < \|ℑ (x)\|)) \to y \in (ℂ ∖ ℝ)$
45	44	ex	$⊢ x \in (ℂ ∖ ℝ) \to ((y \in ℂ \land x (abs \circ -) y < \|ℑ (x)\|) \to y \in (ℂ ∖ ℝ))$
46	16 45	sylbid	$⊢ x \in (ℂ ∖ ℝ) \to (y \in (x ball (abs \circ -) \|ℑ (x)\|) \to y \in (ℂ ∖ ℝ))$
47	46	ssrdv	$⊢ x \in (ℂ ∖ ℝ) \to x ball (abs \circ -) \|ℑ (x)\| \subseteq ℂ ∖ ℝ$
48		oveq2	$⊢ y = \|ℑ (x)\| \to x ball (abs \circ -) y = x ball (abs \circ -) \|ℑ (x)\|$
49	48	sseq1d	$⊢ y = \|ℑ (x)\| \to (x ball (abs \circ -) y \subseteq ℂ ∖ ℝ \leftrightarrow x ball (abs \circ -) \|ℑ (x)\| \subseteq ℂ ∖ ℝ)$
50	49	rspcev	$⊢ (\|ℑ (x)\| \in ℝ^{+} \land x ball (abs \circ -) \|ℑ (x)\| \subseteq ℂ ∖ ℝ) \to \exists y \in ℝ^{+} x ball (abs \circ -) y \subseteq ℂ ∖ ℝ$
51	11 47 50	syl2anc	$⊢ x \in (ℂ ∖ ℝ) \to \exists y \in ℝ^{+} x ball (abs \circ -) y \subseteq ℂ ∖ ℝ$
52	51	rgen	$⊢ \forall x \in (ℂ ∖ ℝ) \exists y \in ℝ^{+} x ball (abs \circ -) y \subseteq ℂ ∖ ℝ$
53	1	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
54	53	elmopn2	$⊢ abs \circ - \in ∞Met (ℂ) \to (ℂ ∖ ℝ \in J \leftrightarrow (ℂ ∖ ℝ \subseteq ℂ \land \forall x \in (ℂ ∖ ℝ) \exists y \in ℝ^{+} x ball (abs \circ -) y \subseteq ℂ ∖ ℝ))$
55	12 54	ax-mp	$⊢ ℂ ∖ ℝ \in J \leftrightarrow (ℂ ∖ ℝ \subseteq ℂ \land \forall x \in (ℂ ∖ ℝ) \exists y \in ℝ^{+} x ball (abs \circ -) y \subseteq ℂ ∖ ℝ)$
56	2 52 55	mpbir2an	$⊢ ℂ ∖ ℝ \in J$
57	1	cnfldtop	$⊢ J \in Top$
58		ax-resscn	$⊢ ℝ \subseteq ℂ$
59	53	mopnuni	$⊢ abs \circ - \in ∞Met (ℂ) \to ℂ = ⋃ J$
60	12 59	ax-mp	$⊢ ℂ = ⋃ J$
61	60	iscld2	$⊢ (J \in Top \land ℝ \subseteq ℂ) \to (ℝ \in Clsd (J) \leftrightarrow ℂ ∖ ℝ \in J)$
62	57 58 61	mp2an	$⊢ ℝ \in Clsd (J) \leftrightarrow ℂ ∖ ℝ \in J$
63	56 62	mpbir	$⊢ ℝ \in Clsd (J)$

Metamath Proof Explorer

Theorem recld2

Proof