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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	cnrefiisp.n	⊢ ( 𝜑 → ¬ 𝐴 ∈ ℝ )
	cnrefiisp.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	cnrefiisp.c	⊢ 𝐶 = ( ℝ ∪ 𝐵 )
Assertion	cnrefiisp	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ⁺ ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnrefiisp.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		cnrefiisp.n	⊢ ( 𝜑 → ¬ 𝐴 ∈ ℝ )
3		cnrefiisp.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
4		cnrefiisp.c	⊢ 𝐶 = ( ℝ ∪ 𝐵 )
5		eqid	⊢ ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑤 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑤 − 𝐴 ) ) } ) = ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑤 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑤 − 𝐴 ) ) } )
6		fvoveq1	⊢ ( 𝑧 = 𝑤 → ( abs ‘ ( 𝑧 − 𝐴 ) ) = ( abs ‘ ( 𝑤 − 𝐴 ) ) )
7	6	sneqd	⊢ ( 𝑧 = 𝑤 → { ( abs ‘ ( 𝑧 − 𝐴 ) ) } = { ( abs ‘ ( 𝑤 − 𝐴 ) ) } )
8	7	cbviunv	⊢ ∪ 𝑧 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑧 − 𝐴 ) ) } = ∪ 𝑤 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑤 − 𝐴 ) ) }
9	8	uneq2i	⊢ ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑧 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑧 − 𝐴 ) ) } ) = ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑤 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑤 − 𝐴 ) ) } )
10	9	infeq1i	⊢ inf ( ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑧 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑧 − 𝐴 ) ) } ) , ℝ^* , < ) = inf ( ( { ( abs ‘ ( ℑ ‘ 𝐴 ) ) } ∪ ∪ 𝑤 ∈ ( ( 𝐵 ∩ ℂ ) ∖ { 𝐴 } ) { ( abs ‘ ( 𝑤 − 𝐴 ) ) } ) , ℝ^* , < )
11	1 2 3 4 5 10	cnrefiisplem	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐶 ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑤 − 𝐴 ) ) ) )
12		eleq1w	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ ℂ ↔ 𝑦 ∈ ℂ ) )
13		neeq1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ≠ 𝐴 ↔ 𝑦 ≠ 𝐴 ) )
14	12 13	anbi12d	⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 𝐴 ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ) )
15		fvoveq1	⊢ ( 𝑤 = 𝑦 → ( abs ‘ ( 𝑤 − 𝐴 ) ) = ( abs ‘ ( 𝑦 − 𝐴 ) ) )
16	15	breq2d	⊢ ( 𝑤 = 𝑦 → ( 𝑥 ≤ ( abs ‘ ( 𝑤 − 𝐴 ) ) ↔ 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )
17	14 16	imbi12d	⊢ ( 𝑤 = 𝑦 → ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑤 − 𝐴 ) ) ) ↔ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) )
18	17	cbvralvw	⊢ ( ∀ 𝑤 ∈ 𝐶 ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑤 − 𝐴 ) ) ) ↔ ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )
19	18	rexbii	⊢ ( ∃ 𝑥 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐶 ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑤 − 𝐴 ) ) ) ↔ ∃ 𝑥 ∈ ℝ⁺ ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )
20	11 19	sylib	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ⁺ ∀ 𝑦 ∈ 𝐶 ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )

Metamath Proof Explorer

Theorem cnrefiisp

Proof