Theorem 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	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion	recld2	⊢ ℝ ∈ ( Clsd ‘ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		recld2.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		difss	⊢ ( ℂ ∖ ℝ ) ⊆ ℂ
3		eldifi	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → 𝑥 ∈ ℂ )
4	3	imcld	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( ℑ ‘ 𝑥 ) ∈ ℝ )
5	4	recnd	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( ℑ ‘ 𝑥 ) ∈ ℂ )
6		eldifn	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ¬ 𝑥 ∈ ℝ )
7		reim0b	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) = 0 ) )
8	3 7	syl	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) = 0 ) )
9	8	necon3bbid	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( ¬ 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) ≠ 0 ) )
10	6 9	mpbid	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( ℑ ‘ 𝑥 ) ≠ 0 )
11	5 10	absrpcld	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( abs ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ+ )
12		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
13	5	abscld	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( abs ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ )
14	13	rexrd	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( abs ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ* )
15		elbl	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑥 ∈ ℂ ∧ ( abs ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ* ) → ( 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) ↔ ( 𝑦 ∈ ℂ ∧ ( 𝑥 ( abs ∘ − ) 𝑦 ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) ) )
16	12 3 14 15	mp3an2i	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) ↔ ( 𝑦 ∈ ℂ ∧ ( 𝑥 ( abs ∘ − ) 𝑦 ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) ) )
17		simprl	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 ( abs ∘ − ) 𝑦 ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) ) → 𝑦 ∈ ℂ )
18	3	adantr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℂ )
19		simpr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
20	19	recnd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
21		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
22	21	cnmetdval	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
23	18 20 22	syl2anc	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
24	5	adantr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ 𝑥 ) ∈ ℂ )
25	24	abscld	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ )
26	18 20	subcld	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑥 − 𝑦 ) ∈ ℂ )
27	26	abscld	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) ∈ ℝ )
28	18 20	imsubd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ ( 𝑥 − 𝑦 ) ) = ( ( ℑ ‘ 𝑥 ) − ( ℑ ‘ 𝑦 ) ) )
29		reim0	⊢ ( 𝑦 ∈ ℝ → ( ℑ ‘ 𝑦 ) = 0 )
30	29	adantl	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ 𝑦 ) = 0 )
31	30	oveq2d	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) − ( ℑ ‘ 𝑦 ) ) = ( ( ℑ ‘ 𝑥 ) − 0 ) )
32	24	subid1d	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) − 0 ) = ( ℑ ‘ 𝑥 ) )
33	28 31 32	3eqtrd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ ( 𝑥 − 𝑦 ) ) = ( ℑ ‘ 𝑥 ) )
34	33	fveq2d	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ ( 𝑥 − 𝑦 ) ) ) = ( abs ‘ ( ℑ ‘ 𝑥 ) ) )
35		absimle	⊢ ( ( 𝑥 − 𝑦 ) ∈ ℂ → ( abs ‘ ( ℑ ‘ ( 𝑥 − 𝑦 ) ) ) ≤ ( abs ‘ ( 𝑥 − 𝑦 ) ) )
36	26 35	syl	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ ( 𝑥 − 𝑦 ) ) ) ≤ ( abs ‘ ( 𝑥 − 𝑦 ) ) )
37	34 36	eqbrtrrd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ 𝑥 ) ) ≤ ( abs ‘ ( 𝑥 − 𝑦 ) ) )
38	25 27 37	lensymd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ¬ ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) )
39	23 38	eqnbrtrd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℝ ) → ¬ ( 𝑥 ( abs ∘ − ) 𝑦 ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) )
40	39	ex	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( 𝑦 ∈ ℝ → ¬ ( 𝑥 ( abs ∘ − ) 𝑦 ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) )
41	40	con2d	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( ( 𝑥 ( abs ∘ − ) 𝑦 ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) → ¬ 𝑦 ∈ ℝ ) )
42	41	adantr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝑥 ( abs ∘ − ) 𝑦 ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) → ¬ 𝑦 ∈ ℝ ) )
43	42	impr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 ( abs ∘ − ) 𝑦 ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) ) → ¬ 𝑦 ∈ ℝ )
44	17 43	eldifd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ℝ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 ( abs ∘ − ) 𝑦 ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) ) → 𝑦 ∈ ( ℂ ∖ ℝ ) )
45	44	ex	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( ( 𝑦 ∈ ℂ ∧ ( 𝑥 ( abs ∘ − ) 𝑦 ) < ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) → 𝑦 ∈ ( ℂ ∖ ℝ ) ) )
46	16 45	sylbid	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) → 𝑦 ∈ ( ℂ ∖ ℝ ) ) )
47	46	ssrdv	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) ⊆ ( ℂ ∖ ℝ ) )
48		oveq2	⊢ ( 𝑦 = ( abs ‘ ( ℑ ‘ 𝑥 ) ) → ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) = ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) )
49	48	sseq1d	⊢ ( 𝑦 = ( abs ‘ ( ℑ ‘ 𝑥 ) ) → ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ ( ℂ ∖ ℝ ) ↔ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) ⊆ ( ℂ ∖ ℝ ) ) )
50	49	rspcev	⊢ ( ( ( abs ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) ( abs ‘ ( ℑ ‘ 𝑥 ) ) ) ⊆ ( ℂ ∖ ℝ ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ ( ℂ ∖ ℝ ) )
51	11 47 50	syl2anc	⊢ ( 𝑥 ∈ ( ℂ ∖ ℝ ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ ( ℂ ∖ ℝ ) )
52	51	rgen	⊢ ∀ 𝑥 ∈ ( ℂ ∖ ℝ ) ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ ( ℂ ∖ ℝ )
53	1	cnfldtopn	⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
54	53	elmopn2	⊢ ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) → ( ( ℂ ∖ ℝ ) ∈ 𝐽 ↔ ( ( ℂ ∖ ℝ ) ⊆ ℂ ∧ ∀ 𝑥 ∈ ( ℂ ∖ ℝ ) ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ ( ℂ ∖ ℝ ) ) ) )
55	12 54	ax-mp	⊢ ( ( ℂ ∖ ℝ ) ∈ 𝐽 ↔ ( ( ℂ ∖ ℝ ) ⊆ ℂ ∧ ∀ 𝑥 ∈ ( ℂ ∖ ℝ ) ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ ( ℂ ∖ ℝ ) ) )
56	2 52 55	mpbir2an	⊢ ( ℂ ∖ ℝ ) ∈ 𝐽
57	1	cnfldtop	⊢ 𝐽 ∈ Top
58		ax-resscn	⊢ ℝ ⊆ ℂ
59	53	mopnuni	⊢ ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) → ℂ = ∪ 𝐽 )
60	12 59	ax-mp	⊢ ℂ = ∪ 𝐽
61	60	iscld2	⊢ ( ( 𝐽 ∈ Top ∧ ℝ ⊆ ℂ ) → ( ℝ ∈ ( Clsd ‘ 𝐽 ) ↔ ( ℂ ∖ ℝ ) ∈ 𝐽 ) )
62	57 58 61	mp2an	⊢ ( ℝ ∈ ( Clsd ‘ 𝐽 ) ↔ ( ℂ ∖ ℝ ) ∈ 𝐽 )
63	56 62	mpbir	⊢ ℝ ∈ ( Clsd ‘ 𝐽 )