Theorem cnrefiisp

Description: A non-real, complex number is an isolated point w.r.t. the union of the reals with any finite set (the extended reals is an example of such a union). (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	cnrefiisp.a	$$⊢\phi \to A\in ℂ$$
	cnrefiisp.n	$$⊢\phi \to \neg A\in ℝ$$
	cnrefiisp.b	$$⊢\phi \to B\in \mathrm{Fin}$$
	cnrefiisp.c	$$⊢C=ℝ\cup B$$
Assertion	cnrefiisp	$$⊢\phi \to \exists x\in {ℝ}^{+}\forall y\in C\left(\left(y\in ℂ\wedge y\ne A\right)\to x\le \left|y-A\right|\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnrefiisp.a	$$⊢\phi \to A\in ℂ$$
2		cnrefiisp.n	$$⊢\phi \to \neg A\in ℝ$$
3		cnrefiisp.b	$$⊢\phi \to B\in \mathrm{Fin}$$
4		cnrefiisp.c	$$⊢C=ℝ\cup B$$
5		eqid	$$⊢\left\{\left|\Im \left(A\right)\right|\right\}\cup \bigcup _{w\in \left(B\cap ℂ\right)\setminus \left\{A\right\}}\left\{\left|w-A\right|\right\}=\left\{\left|\Im \left(A\right)\right|\right\}\cup \bigcup _{w\in \left(B\cap ℂ\right)\setminus \left\{A\right\}}\left\{\left|w-A\right|\right\}$$
6		fvoveq1	$$⊢z=w\to \left|z-A\right|=\left|w-A\right|$$
7	6	sneqd	$$⊢z=w\to \left\{\left|z-A\right|\right\}=\left\{\left|w-A\right|\right\}$$
8	7	cbviunv	$$⊢\bigcup _{z\in \left(B\cap ℂ\right)\setminus \left\{A\right\}}\left\{\left|z-A\right|\right\}=\bigcup _{w\in \left(B\cap ℂ\right)\setminus \left\{A\right\}}\left\{\left|w-A\right|\right\}$$
9	8	uneq2i	$$⊢\left\{\left|\Im \left(A\right)\right|\right\}\cup \bigcup _{z\in \left(B\cap ℂ\right)\setminus \left\{A\right\}}\left\{\left|z-A\right|\right\}=\left\{\left|\Im \left(A\right)\right|\right\}\cup \bigcup _{w\in \left(B\cap ℂ\right)\setminus \left\{A\right\}}\left\{\left|w-A\right|\right\}$$
10	9	infeq1i	$$⊢inf\left(\left\{\left|\Im \left(A\right)\right|\right\}\cup \bigcup _{z\in \left(B\cap ℂ\right)\setminus \left\{A\right\}}\left\{\left|z-A\right|\right\},{ℝ}^{*},<\right)=inf\left(\left\{\left|\Im \left(A\right)\right|\right\}\cup \bigcup _{w\in \left(B\cap ℂ\right)\setminus \left\{A\right\}}\left\{\left|w-A\right|\right\},{ℝ}^{*},<\right)$$
11	1 2 3 4 5 10	cnrefiisplem	$$⊢\phi \to \exists x\in {ℝ}^{+}\forall w\in C\left(\left(w\in ℂ\wedge w\ne A\right)\to x\le \left|w-A\right|\right)$$
12		eleq1w	$$⊢w=y\to \left(w\in ℂ\leftrightarrow y\in ℂ\right)$$
13		neeq1	$$⊢w=y\to \left(w\ne A\leftrightarrow y\ne A\right)$$
14	12 13	anbi12d	$$⊢w=y\to \left(\left(w\in ℂ\wedge w\ne A\right)\leftrightarrow \left(y\in ℂ\wedge y\ne A\right)\right)$$
15		fvoveq1	$$⊢w=y\to \left|w-A\right|=\left|y-A\right|$$
16	15	breq2d	$$⊢w=y\to \left(x\le \left|w-A\right|\leftrightarrow x\le \left|y-A\right|\right)$$
17	14 16	imbi12d	$$⊢w=y\to \left(\left(\left(w\in ℂ\wedge w\ne A\right)\to x\le \left|w-A\right|\right)\leftrightarrow \left(\left(y\in ℂ\wedge y\ne A\right)\to x\le \left|y-A\right|\right)\right)$$
18	17	cbvralvw	$$⊢\forall w\in C\left(\left(w\in ℂ\wedge w\ne A\right)\to x\le \left|w-A\right|\right)\leftrightarrow \forall y\in C\left(\left(y\in ℂ\wedge y\ne A\right)\to x\le \left|y-A\right|\right)$$
19	18	rexbii	$$⊢\exists x\in {ℝ}^{+}\forall w\in C\left(\left(w\in ℂ\wedge w\ne A\right)\to x\le \left|w-A\right|\right)\leftrightarrow \exists x\in {ℝ}^{+}\forall y\in C\left(\left(y\in ℂ\wedge y\ne A\right)\to x\le \left|y-A\right|\right)$$
20	11 19	sylib	$$⊢\phi \to \exists x\in {ℝ}^{+}\forall y\in C\left(\left(y\in ℂ\wedge y\ne A\right)\to x\le \left|y-A\right|\right)$$