reperflem

Description: A subset of the real numbers that is closed under addition with real numbers is perfect. (Contributed by Mario Carneiro, 26-Dec-2016)

	Ref	Expression
Hypotheses	recld2.1	$⊢ J = TopOpen (ℂ_{fld})$
	reperflem.2	$⊢ (u \in S \land v \in ℝ) \to u + v \in S$
	reperflem.3	$⊢ S \subseteq ℂ$
Assertion	reperflem	$⊢ J ↾_{𝑡} S \in Perf$

Proof

Step	Hyp	Ref	Expression
1		recld2.1	$⊢ J = TopOpen (ℂ_{fld})$
2		reperflem.2	$⊢ (u \in S \land v \in ℝ) \to u + v \in S$
3		reperflem.3	$⊢ S \subseteq ℂ$
4		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
5	3	sseli	$⊢ u \in S \to u \in ℂ$
6	1	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
7	6	neibl	$⊢ (abs \circ - \in ∞Met (ℂ) \land u \in ℂ) \to (n \in nei (J) (\{u\}) \leftrightarrow (n \subseteq ℂ \land \exists r \in ℝ^{+} u ball (abs \circ -) r \subseteq n))$
8	4 5 7	sylancr	$⊢ u \in S \to (n \in nei (J) (\{u\}) \leftrightarrow (n \subseteq ℂ \land \exists r \in ℝ^{+} u ball (abs \circ -) r \subseteq n))$
9		ssrin	$⊢ u ball (abs \circ -) r \subseteq n \to (u ball (abs \circ -) r) \cap (S ∖ \{u\}) \subseteq n \cap (S ∖ \{u\})$
10	2	ralrimiva	$⊢ u \in S \to \forall v \in ℝ u + v \in S$
11		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
12	11	rehalfcld	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ$
13		oveq2	$⊢ v = \frac{r}{2} \to u + v = u + (\frac{r}{2})$
14	13	eleq1d	$⊢ v = \frac{r}{2} \to (u + v \in S \leftrightarrow u + (\frac{r}{2}) \in S)$
15	14	rspccva	$⊢ (\forall v \in ℝ u + v \in S \land \frac{r}{2} \in ℝ) \to u + (\frac{r}{2}) \in S$
16	10 12 15	syl2an	$⊢ (u \in S \land r \in ℝ^{+}) \to u + (\frac{r}{2}) \in S$
17	3 16	sseldi	$⊢ (u \in S \land r \in ℝ^{+}) \to u + (\frac{r}{2}) \in ℂ$
18	5	adantr	$⊢ (u \in S \land r \in ℝ^{+}) \to u \in ℂ$
19		eqid	$⊢ abs \circ - = abs \circ -$
20	19	cnmetdval	$⊢ (u + (\frac{r}{2}) \in ℂ \land u \in ℂ) \to (u + (\frac{r}{2})) (abs \circ -) u = \|u + (\frac{r}{2}) - u\|$
21	17 18 20	syl2anc	$⊢ (u \in S \land r \in ℝ^{+}) \to (u + (\frac{r}{2})) (abs \circ -) u = \|u + (\frac{r}{2}) - u\|$
22		simpr	$⊢ (u \in S \land r \in ℝ^{+}) \to r \in ℝ^{+}$
23	22	rphalfcld	$⊢ (u \in S \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ^{+}$
24	23	rpcnd	$⊢ (u \in S \land r \in ℝ^{+}) \to \frac{r}{2} \in ℂ$
25	18 24	pncan2d	$⊢ (u \in S \land r \in ℝ^{+}) \to u + (\frac{r}{2}) - u = \frac{r}{2}$
26	25	fveq2d	$⊢ (u \in S \land r \in ℝ^{+}) \to \|u + (\frac{r}{2}) - u\| = \|\frac{r}{2}\|$
27	23	rpred	$⊢ (u \in S \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ$
28	23	rpge0d	$⊢ (u \in S \land r \in ℝ^{+}) \to 0 \leq \frac{r}{2}$
29	27 28	absidd	$⊢ (u \in S \land r \in ℝ^{+}) \to \|\frac{r}{2}\| = \frac{r}{2}$
30	21 26 29	3eqtrd	$⊢ (u \in S \land r \in ℝ^{+}) \to (u + (\frac{r}{2})) (abs \circ -) u = \frac{r}{2}$
31		rphalflt	$⊢ r \in ℝ^{+} \to \frac{r}{2} < r$
32	31	adantl	$⊢ (u \in S \land r \in ℝ^{+}) \to \frac{r}{2} < r$
33	30 32	eqbrtrd	$⊢ (u \in S \land r \in ℝ^{+}) \to (u + (\frac{r}{2})) (abs \circ -) u < r$
34	4	a1i	$⊢ (u \in S \land r \in ℝ^{+}) \to abs \circ - \in ∞Met (ℂ)$
35		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
36	35	adantl	$⊢ (u \in S \land r \in ℝ^{+}) \to r \in ℝ^{*}$
37		elbl3	$⊢ ((abs \circ - \in ∞Met (ℂ) \land r \in ℝ^{*}) \land (u \in ℂ \land u + (\frac{r}{2}) \in ℂ)) \to (u + (\frac{r}{2}) \in (u ball (abs \circ -) r) \leftrightarrow (u + (\frac{r}{2})) (abs \circ -) u < r)$
38	34 36 18 17 37	syl22anc	$⊢ (u \in S \land r \in ℝ^{+}) \to (u + (\frac{r}{2}) \in (u ball (abs \circ -) r) \leftrightarrow (u + (\frac{r}{2})) (abs \circ -) u < r)$
39	33 38	mpbird	$⊢ (u \in S \land r \in ℝ^{+}) \to u + (\frac{r}{2}) \in (u ball (abs \circ -) r)$
40	23	rpne0d	$⊢ (u \in S \land r \in ℝ^{+}) \to \frac{r}{2} \neq 0$
41	25 40	eqnetrd	$⊢ (u \in S \land r \in ℝ^{+}) \to u + (\frac{r}{2}) - u \neq 0$
42	17 18 41	subne0ad	$⊢ (u \in S \land r \in ℝ^{+}) \to u + (\frac{r}{2}) \neq u$
43		eldifsn	$⊢ u + (\frac{r}{2}) \in (S ∖ \{u\}) \leftrightarrow (u + (\frac{r}{2}) \in S \land u + (\frac{r}{2}) \neq u)$
44	16 42 43	sylanbrc	$⊢ (u \in S \land r \in ℝ^{+}) \to u + (\frac{r}{2}) \in (S ∖ \{u\})$
45		inelcm	$⊢ (u + (\frac{r}{2}) \in (u ball (abs \circ -) r) \land u + (\frac{r}{2}) \in (S ∖ \{u\})) \to (u ball (abs \circ -) r) \cap (S ∖ \{u\}) \neq \emptyset$
46	39 44 45	syl2anc	$⊢ (u \in S \land r \in ℝ^{+}) \to (u ball (abs \circ -) r) \cap (S ∖ \{u\}) \neq \emptyset$
47		ssn0	$⊢ ((u ball (abs \circ -) r) \cap (S ∖ \{u\}) \subseteq n \cap (S ∖ \{u\}) \land (u ball (abs \circ -) r) \cap (S ∖ \{u\}) \neq \emptyset) \to n \cap (S ∖ \{u\}) \neq \emptyset$
48	47	ex	$⊢ (u ball (abs \circ -) r) \cap (S ∖ \{u\}) \subseteq n \cap (S ∖ \{u\}) \to ((u ball (abs \circ -) r) \cap (S ∖ \{u\}) \neq \emptyset \to n \cap (S ∖ \{u\}) \neq \emptyset)$
49	9 46 48	syl2imc	$⊢ (u \in S \land r \in ℝ^{+}) \to (u ball (abs \circ -) r \subseteq n \to n \cap (S ∖ \{u\}) \neq \emptyset)$
50	49	rexlimdva	$⊢ u \in S \to (\exists r \in ℝ^{+} u ball (abs \circ -) r \subseteq n \to n \cap (S ∖ \{u\}) \neq \emptyset)$
51	50	adantld	$⊢ u \in S \to ((n \subseteq ℂ \land \exists r \in ℝ^{+} u ball (abs \circ -) r \subseteq n) \to n \cap (S ∖ \{u\}) \neq \emptyset)$
52	8 51	sylbid	$⊢ u \in S \to (n \in nei (J) (\{u\}) \to n \cap (S ∖ \{u\}) \neq \emptyset)$
53	52	ralrimiv	$⊢ u \in S \to \forall n \in nei (J) (\{u\}) n \cap (S ∖ \{u\}) \neq \emptyset$
54	1	cnfldtop	$⊢ J \in Top$
55	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
56	55	toponunii	$⊢ ℂ = ⋃ J$
57	56	islp2	$⊢ (J \in Top \land S \subseteq ℂ \land u \in ℂ) \to (u \in limPt (J) (S) \leftrightarrow \forall n \in nei (J) (\{u\}) n \cap (S ∖ \{u\}) \neq \emptyset)$
58	54 3 5 57	mp3an12i	$⊢ u \in S \to (u \in limPt (J) (S) \leftrightarrow \forall n \in nei (J) (\{u\}) n \cap (S ∖ \{u\}) \neq \emptyset)$
59	53 58	mpbird	$⊢ u \in S \to u \in limPt (J) (S)$
60	59	ssriv	$⊢ S \subseteq limPt (J) (S)$
61		eqid	$⊢ J ↾_{𝑡} S = J ↾_{𝑡} S$
62	56 61	restperf	$⊢ (J \in Top \land S \subseteq ℂ) \to (J ↾_{𝑡} S \in Perf \leftrightarrow S \subseteq limPt (J) (S))$
63	54 3 62	mp2an	$⊢ J ↾_{𝑡} S \in Perf \leftrightarrow S \subseteq limPt (J) (S)$
64	60 63	mpbir	$⊢ J ↾_{𝑡} S \in Perf$

Metamath Proof Explorer

Theorem reperflem

Proof