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	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ_≥ ‘ 𝑗 ) ) : ( ℤ_≥ ‘ 𝑗 ) ⟶ ℂ )

Metamath Proof Explorer

Theorem climrescn

Proof