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	$⊢ φ \to M \in ℤ$
	climisp.z	$⊢ Z = ℤ_{\geq M}$
	climisp.f	$⊢ φ \to F : Z ⟶ ℂ$
	climisp.c	$⊢ φ \to F ⇝ A$
	climisp.x	$⊢ φ \to X \in ℝ^{+}$
	climisp.l	$⊢ (φ \land k \in Z \land F (k) \neq A) \to X \leq \|F (k) - A\|$
Assertion	climisp	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) = A$

Proof

Step	Hyp	Ref	Expression
1		climisp.m	$⊢ φ \to M \in ℤ$
2		climisp.z	$⊢ Z = ℤ_{\geq M}$
3		climisp.f	$⊢ φ \to F : Z ⟶ ℂ$
4		climisp.c	$⊢ φ \to F ⇝ A$
5		climisp.x	$⊢ φ \to X \in ℝ^{+}$
6		climisp.l	$⊢ (φ \land k \in Z \land F (k) \neq A) \to X \leq \|F (k) - A\|$
7		nfv	$⊢ Ⅎ k (φ \land j \in Z)$
8		nfra1	$⊢ Ⅎ k \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X)$
9	7 8	nfan	$⊢ Ⅎ k ((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X))$
10		simplll	$⊢ (((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X)) \land k \in ℤ_{\geq j}) \to φ$
11	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
12	11	ad4ant24	$⊢ (((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X)) \land k \in ℤ_{\geq j}) \to k \in Z$
13		rspa	$⊢ (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X) \land k \in ℤ_{\geq j}) \to (F (k) \in ℂ \land \|F (k) - A\| < X)$
14	13	simprd	$⊢ (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X) \land k \in ℤ_{\geq j}) \to \|F (k) - A\| < X$
15	14	adantll	$⊢ (((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X)) \land k \in ℤ_{\geq j}) \to \|F (k) - A\| < X$
16		simpl3	$⊢ ((φ \land k \in Z \land \|F (k) - A\| < X) \land \neg F (k) = A) \to \|F (k) - A\| < X$
17		neqne	$⊢ \neg F (k) = A \to F (k) \neq A$
18	5	rpred	$⊢ φ \to X \in ℝ$
19	18	ad2antrr	$⊢ ((φ \land k \in Z) \land F (k) \neq A) \to X \in ℝ$
20	3	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
21	2	fvexi	$⊢ Z \in V$
22	21	a1i	$⊢ φ \to Z \in V$
23	3 22	fexd	$⊢ φ \to F \in V$
24		eqidd	$⊢ (φ \land k \in ℤ) \to F (k) = F (k)$
25	23 24	clim	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)))$
26	4 25	mpbid	$⊢ φ \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
27	26	simpld	$⊢ φ \to A \in ℂ$
28	27	adantr	$⊢ (φ \land k \in Z) \to A \in ℂ$
29	20 28	subcld	$⊢ (φ \land k \in Z) \to F (k) - A \in ℂ$
30	29	abscld	$⊢ (φ \land k \in Z) \to \|F (k) - A\| \in ℝ$
31	30	adantr	$⊢ ((φ \land k \in Z) \land F (k) \neq A) \to \|F (k) - A\| \in ℝ$
32	6	3expa	$⊢ ((φ \land k \in Z) \land F (k) \neq A) \to X \leq \|F (k) - A\|$
33	19 31 32	lensymd	$⊢ ((φ \land k \in Z) \land F (k) \neq A) \to \neg \|F (k) - A\| < X$
34	17 33	sylan2	$⊢ ((φ \land k \in Z) \land \neg F (k) = A) \to \neg \|F (k) - A\| < X$
35	34	3adantl3	$⊢ ((φ \land k \in Z \land \|F (k) - A\| < X) \land \neg F (k) = A) \to \neg \|F (k) - A\| < X$
36	16 35	condan	$⊢ (φ \land k \in Z \land \|F (k) - A\| < X) \to F (k) = A$
37	10 12 15 36	syl3anc	$⊢ (((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X)) \land k \in ℤ_{\geq j}) \to F (k) = A$
38	9 37	ralrimia	$⊢ ((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X)) \to \forall k \in ℤ_{\geq j} F (k) = A$
39		breq2	$⊢ x = X \to (\|F (k) - A\| < x \leftrightarrow \|F (k) - A\| < X)$
40	39	anbi2d	$⊢ x = X \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - A\| < X))$
41	40	rexralbidv	$⊢ x = X \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X))$
42	26	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
43	41 42 5	rspcdva	$⊢ φ \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X)$
44	2	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X))$
45	1 44	syl	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X))$
46	43 45	mpbird	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X)$
47	38 46	reximddv3	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) = A$

Metamath Proof Explorer

Theorem climisp

Proof