Metamath Proof Explorer

Theorem climrescn

Description: A sequence converging w.r.t. the standard topology on the complex numbers, eventually becomes a sequence of complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses climrescn.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climrescn.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climrescn.f ⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
climrescn.c ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
Assertion climrescn ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ )

Proof

Step Hyp Ref Expression
1 climrescn.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 climrescn.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 climrescn.f ⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
4 climrescn.c ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
5 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑖 ∈ 𝑍 )
6 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 )
7 5 6 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) )
8 2 uztrn2 ⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑘 ∈ 𝑍 )
9 8 adantll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑘 ∈ 𝑍 )
10 3 fndmd ⊢ ( 𝜑 → dom 𝐹 = 𝑍 )
11 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → dom 𝐹 = 𝑍 )
12 9 11 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑘 ∈ dom 𝐹 )
13 12 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑘 ∈ dom 𝐹 )
14 rspa ⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) )
15 14 adantll ⊢ ( ( ( 𝑖 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) )
16 15 simpld ⊢ ( ( ( 𝑖 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
17 16 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
18 13 17 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
19 7 18 ralrimia ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
20 fnfun ⊢ ( 𝐹 Fn 𝑍 → Fun 𝐹 )
21 ffvresb ⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) : ( ℤ≥ ‘ 𝑖 ) ⟶ ℂ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) )
22 3 20 21 3syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) : ( ℤ≥ ‘ 𝑖 ) ⟶ ℂ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) : ( ℤ≥ ‘ 𝑖 ) ⟶ ℂ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) )
24 19 23 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) : ( ℤ≥ ‘ 𝑖 ) ⟶ ℂ )
25 breq2 ⊢ ( 𝑥 = 1 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) )
26 25 anbi2d ⊢ ( 𝑥 = 1 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) )
27 26 rexralbidv ⊢ ( 𝑥 = 1 → ( ∃ 𝑖 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 𝑥 ) ↔ ∃ 𝑖 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) )
28 climdm ⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
29 4 28 sylib ⊢ ( 𝜑 → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
30 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
31 4 30 clim ⊢ ( 𝜑 → ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ↔ ( ( ⇝ ‘ 𝐹 ) ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑖 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 𝑥 ) ) ) )
32 29 31 mpbid ⊢ ( 𝜑 → ( ( ⇝ ‘ 𝐹 ) ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑖 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 𝑥 ) ) )
33 32 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑖 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 𝑥 ) )
34 1rp ⊢ 1 ∈ ℝ+
35 34 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
36 27 33 35 rspcdva ⊢ ( 𝜑 → ∃ 𝑖 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) )
37 2 rexuz3 ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ↔ ∃ 𝑖 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) )
38 1 37 syl ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ↔ ∃ 𝑖 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) ) )
39 36 38 mpbird ⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( ⇝ ‘ 𝐹 ) ) ) < 1 ) )
40 24 39 reximddv3 ⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) : ( ℤ≥ ‘ 𝑖 ) ⟶ ℂ )
41 fveq2 ⊢ ( 𝑗 = 𝑖 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑖 ) )
42 41 reseq2d ⊢ ( 𝑗 = 𝑖 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
43 42 41 feq12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) : ( ℤ≥ ‘ 𝑖 ) ⟶ ℂ ) )
44 43 cbvrexvw ⊢ ( ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ ↔ ∃ 𝑖 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) : ( ℤ≥ ‘ 𝑖 ) ⟶ ℂ )
45 40 44 sylibr ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ )