Metamath Proof Explorer


Theorem 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 ffvelrnda ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
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 ( 𝜑 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) = 𝐴 )