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	$⊢ φ \to M \in ℤ$
	climrescn.z	$⊢ Z = ℤ_{\geq M}$
	climrescn.f	$⊢ φ \to F Fn Z$
	climrescn.c	$⊢ φ \to F \in dom ⇝$
Assertion	climrescn	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ$

Proof

Step	Hyp	Ref	Expression
1		climrescn.m	$⊢ φ \to M \in ℤ$
2		climrescn.z	$⊢ Z = ℤ_{\geq M}$
3		climrescn.f	$⊢ φ \to F Fn Z$
4		climrescn.c	$⊢ φ \to F \in dom ⇝$
5		nfv	$⊢ Ⅎ k (φ \land i \in Z)$
6		nfra1	$⊢ Ⅎ k \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)$
7	5 6	nfan	$⊢ Ⅎ k ((φ \land i \in Z) \land \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1))$
8	2	uztrn2	$⊢ (i \in Z \land k \in ℤ_{\geq i}) \to k \in Z$
9	8	adantll	$⊢ ((φ \land i \in Z) \land k \in ℤ_{\geq i}) \to k \in Z$
10	3	fndmd	$⊢ φ \to dom F = Z$
11	10	ad2antrr	$⊢ ((φ \land i \in Z) \land k \in ℤ_{\geq i}) \to dom F = Z$
12	9 11	eleqtrrd	$⊢ ((φ \land i \in Z) \land k \in ℤ_{\geq i}) \to k \in dom F$
13	12	adantlr	$⊢ (((φ \land i \in Z) \land \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)) \land k \in ℤ_{\geq i}) \to k \in dom F$
14		rspa	$⊢ (\forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1) \land k \in ℤ_{\geq i}) \to (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)$
15	14	adantll	$⊢ ((i \in Z \land \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)) \land k \in ℤ_{\geq i}) \to (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)$
16	15	simpld	$⊢ ((i \in Z \land \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)) \land k \in ℤ_{\geq i}) \to F (k) \in ℂ$
17	16	adantlll	$⊢ (((φ \land i \in Z) \land \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)) \land k \in ℤ_{\geq i}) \to F (k) \in ℂ$
18	13 17	jca	$⊢ (((φ \land i \in Z) \land \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)) \land k \in ℤ_{\geq i}) \to (k \in dom F \land F (k) \in ℂ)$
19	7 18	ralrimia	$⊢ ((φ \land i \in Z) \land \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)) \to \forall k \in ℤ_{\geq i} (k \in dom F \land F (k) \in ℂ)$
20		fnfun	$⊢ F Fn Z \to Fun F$
21		ffvresb	$⊢ Fun F \to (({F ↾}_{ℤ_{\geq i}}) : ℤ_{\geq i} ⟶ ℂ \leftrightarrow \forall k \in ℤ_{\geq i} (k \in dom F \land F (k) \in ℂ))$
22	3 20 21	3syl	$⊢ φ \to (({F ↾}_{ℤ_{\geq i}}) : ℤ_{\geq i} ⟶ ℂ \leftrightarrow \forall k \in ℤ_{\geq i} (k \in dom F \land F (k) \in ℂ))$
23	22	ad2antrr	$⊢ ((φ \land i \in Z) \land \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)) \to (({F ↾}_{ℤ_{\geq i}}) : ℤ_{\geq i} ⟶ ℂ \leftrightarrow \forall k \in ℤ_{\geq i} (k \in dom F \land F (k) \in ℂ))$
24	19 23	mpbird	$⊢ ((φ \land i \in Z) \land \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)) \to ({F ↾}_{ℤ_{\geq i}}) : ℤ_{\geq i} ⟶ ℂ$
25		breq2	$⊢ x = 1 \to (\|F (k) - ⇝ (F)\| < x \leftrightarrow \|F (k) - ⇝ (F)\| < 1)$
26	25	anbi2d	$⊢ x = 1 \to ((F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1))$
27	26	rexralbidv	$⊢ x = 1 \to (\exists i \in ℤ \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < x) \leftrightarrow \exists i \in ℤ \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1))$
28		climdm	$⊢ F \in dom ⇝ \leftrightarrow F ⇝ ⇝ (F)$
29	4 28	sylib	$⊢ φ \to F ⇝ ⇝ (F)$
30		eqidd	$⊢ (φ \land k \in ℤ) \to F (k) = F (k)$
31	4 30	clim	$⊢ φ \to (F ⇝ ⇝ (F) \leftrightarrow (⇝ (F) \in ℂ \land \forall x \in ℝ^{+} \exists i \in ℤ \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < x)))$
32	29 31	mpbid	$⊢ φ \to (⇝ (F) \in ℂ \land \forall x \in ℝ^{+} \exists i \in ℤ \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < x))$
33	32	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists i \in ℤ \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < x)$
34		1rp	$⊢ 1 \in ℝ^{+}$
35	34	a1i	$⊢ φ \to 1 \in ℝ^{+}$
36	27 33 35	rspcdva	$⊢ φ \to \exists i \in ℤ \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)$
37	2	rexuz3	$⊢ M \in ℤ \to (\exists i \in Z \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1) \leftrightarrow \exists i \in ℤ \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1))$
38	1 37	syl	$⊢ φ \to (\exists i \in Z \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1) \leftrightarrow \exists i \in ℤ \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1))$
39	36 38	mpbird	$⊢ φ \to \exists i \in Z \forall k \in ℤ_{\geq i} (F (k) \in ℂ \land \|F (k) - ⇝ (F)\| < 1)$
40	24 39	reximddv3	$⊢ φ \to \exists i \in Z ({F ↾}_{ℤ_{\geq i}}) : ℤ_{\geq i} ⟶ ℂ$
41		fveq2	$⊢ j = i \to ℤ_{\geq j} = ℤ_{\geq i}$
42	41	reseq2d	$⊢ j = i \to {F ↾}_{ℤ_{\geq j}} = {F ↾}_{ℤ_{\geq i}}$
43	42 41	feq12d	$⊢ j = i \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ \leftrightarrow ({F ↾}_{ℤ_{\geq i}}) : ℤ_{\geq i} ⟶ ℂ)$
44	43	cbvrexvw	$⊢ \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ \leftrightarrow \exists i \in Z ({F ↾}_{ℤ_{\geq i}}) : ℤ_{\geq i} ⟶ ℂ$
45	40 44	sylibr	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ$

Metamath Proof Explorer

Theorem climrescn

Proof