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	|- ( ph -> A e. CC )
	cnrefiisp.n	|- ( ph -> -. A e. RR )
	cnrefiisp.b	|- ( ph -> B e. Fin )
	cnrefiisp.c	|- C = ( RR u. B )
Assertion	cnrefiisp	|- ( ph -> E. x e. RR+ A. y e. C ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnrefiisp.a	|- ( ph -> A e. CC )
2		cnrefiisp.n	|- ( ph -> -. A e. RR )
3		cnrefiisp.b	|- ( ph -> B e. Fin )
4		cnrefiisp.c	|- C = ( RR u. B )
5		eqid	|- ( { ( abs ` ( Im ` A ) ) } u. U_ w e. ( ( B i^i CC ) \ { A } ) { ( abs ` ( w - A ) ) } ) = ( { ( abs ` ( Im ` A ) ) } u. U_ w e. ( ( B i^i CC ) \ { A } ) { ( abs ` ( w - A ) ) } )
6		fvoveq1	|- ( z = w -> ( abs ` ( z - A ) ) = ( abs ` ( w - A ) ) )
7	6	sneqd	|- ( z = w -> { ( abs ` ( z - A ) ) } = { ( abs ` ( w - A ) ) } )
8	7	cbviunv	|- U_ z e. ( ( B i^i CC ) \ { A } ) { ( abs ` ( z - A ) ) } = U_ w e. ( ( B i^i CC ) \ { A } ) { ( abs ` ( w - A ) ) }
9	8	uneq2i	|- ( { ( abs ` ( Im ` A ) ) } u. U_ z e. ( ( B i^i CC ) \ { A } ) { ( abs ` ( z - A ) ) } ) = ( { ( abs ` ( Im ` A ) ) } u. U_ w e. ( ( B i^i CC ) \ { A } ) { ( abs ` ( w - A ) ) } )
10	9	infeq1i	|- inf ( ( { ( abs ` ( Im ` A ) ) } u. U_ z e. ( ( B i^i CC ) \ { A } ) { ( abs ` ( z - A ) ) } ) , RR* , < ) = inf ( ( { ( abs ` ( Im ` A ) ) } u. U_ w e. ( ( B i^i CC ) \ { A } ) { ( abs ` ( w - A ) ) } ) , RR* , < )
11	1 2 3 4 5 10	cnrefiisplem	|- ( ph -> E. x e. RR+ A. w e. C ( ( w e. CC /\ w =/= A ) -> x <_ ( abs ` ( w - A ) ) ) )
12		eleq1w	|- ( w = y -> ( w e. CC <-> y e. CC ) )
13		neeq1	|- ( w = y -> ( w =/= A <-> y =/= A ) )
14	12 13	anbi12d	|- ( w = y -> ( ( w e. CC /\ w =/= A ) <-> ( y e. CC /\ y =/= A ) ) )
15		fvoveq1	|- ( w = y -> ( abs ` ( w - A ) ) = ( abs ` ( y - A ) ) )
16	15	breq2d	|- ( w = y -> ( x <_ ( abs ` ( w - A ) ) <-> x <_ ( abs ` ( y - A ) ) ) )
17	14 16	imbi12d	|- ( w = y -> ( ( ( w e. CC /\ w =/= A ) -> x <_ ( abs ` ( w - A ) ) ) <-> ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) )
18	17	cbvralvw	|- ( A. w e. C ( ( w e. CC /\ w =/= A ) -> x <_ ( abs ` ( w - A ) ) ) <-> A. y e. C ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) )
19	18	rexbii	|- ( E. x e. RR+ A. w e. C ( ( w e. CC /\ w =/= A ) -> x <_ ( abs ` ( w - A ) ) ) <-> E. x e. RR+ A. y e. C ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) )
20	11 19	sylib	|- ( ph -> E. x e. RR+ A. y e. C ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) )