climisp

Description: If a sequence converges to an isolated point (w.r.t. the standard topology on the complex numbers) then the sequence eventually becomes that point. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	climisp.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climisp.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	climisp.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
	climisp.c	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
	climisp.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ⁺ )
	climisp.l	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → 𝑋 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
Assertion	climisp	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		climisp.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		climisp.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
3		climisp.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
4		climisp.c	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
5		climisp.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ⁺ )
6		climisp.l	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → 𝑋 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
7		nfv	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
8		nfra1	⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 )
9	7 8	nfan	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) )
10		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝜑 )
11	2	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
12	11	ad4ant24	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
13		rspa	⊢ ( ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) )
14	13	simprd	⊢ ( ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 )
15	14	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 )
16		simpl3	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 )
17		neqne	⊢ ( ¬ ( 𝐹 ‘ 𝑘 ) = 𝐴 → ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 )
18	5	rpred	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
19	18	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → 𝑋 ∈ ℝ )
20	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
21	2	fvexi	⊢ 𝑍 ∈ V
22	21	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
23	3 22	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
24		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
25	23 24	clim	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
26	4 25	mpbid	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
27	26	simpld	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
29	20 28	subcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ℂ )
30	29	abscld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ )
31	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ )
32	6	3expa	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → 𝑋 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
33	19 31 32	lensymd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → ¬ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 )
34	17 33	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → ¬ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 )
35	34	3adantl3	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → ¬ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 )
36	16 35	condan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
37	10 12 15 36	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
38	9 37	ralrimia	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ) → ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 )
39		breq2	⊢ ( 𝑥 = 𝑋 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) )
40	39	anbi2d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ) )
41	40	rexralbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ) )
42	26	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
43	41 42 5	rspcdva	⊢ ( 𝜑 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) )
44	2	rexuz3	⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ) )
45	1 44	syl	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ) )
46	43 45	mpbird	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) )
47	38 46	reximddv3	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 )

Metamath Proof Explorer

Theorem climisp

Proof