clim

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . This means that for any real x , no matter how small, there always exists an integer j such that the absolute difference of any later complex number in the sequence and the limit is less than x . (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Hypotheses	clim.1	$⊢ φ \to F \in V$
	clim.3	$⊢ (φ \land k \in ℤ) \to F (k) = B$
Assertion	clim	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)))$

Proof

Step	Hyp	Ref	Expression
1		clim.1	$⊢ φ \to F \in V$
2		clim.3	$⊢ (φ \land k \in ℤ) \to F (k) = B$
3		climrel	$⊢ Rel ⇝$
4	3	brrelex2i	$⊢ F ⇝ A \to A \in V$
5	4	a1i	$⊢ φ \to (F ⇝ A \to A \in V)$
6		elex	$⊢ A \in ℂ \to A \in V$
7	6	adantr	$⊢ (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \to A \in V$
8	7	a1i	$⊢ φ \to ((A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \to A \in V)$
9		simpr	$⊢ (f = F \land y = A) \to y = A$
10	9	eleq1d	$⊢ (f = F \land y = A) \to (y \in ℂ \leftrightarrow A \in ℂ)$
11		fveq1	$⊢ f = F \to f (k) = F (k)$
12	11	adantr	$⊢ (f = F \land y = A) \to f (k) = F (k)$
13	12	eleq1d	$⊢ (f = F \land y = A) \to (f (k) \in ℂ \leftrightarrow F (k) \in ℂ)$
14		oveq12	$⊢ (f (k) = F (k) \land y = A) \to f (k) - y = F (k) - A$
15	11 14	sylan	$⊢ (f = F \land y = A) \to f (k) - y = F (k) - A$
16	15	fveq2d	$⊢ (f = F \land y = A) \to \|f (k) - y\| = \|F (k) - A\|$
17	16	breq1d	$⊢ (f = F \land y = A) \to (\|f (k) - y\| < x \leftrightarrow \|F (k) - A\| < x)$
18	13 17	anbi12d	$⊢ (f = F \land y = A) \to ((f (k) \in ℂ \land \|f (k) - y\| < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - A\| < x))$
19	18	ralbidv	$⊢ (f = F \land y = A) \to (\forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x) \leftrightarrow \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
20	19	rexbidv	$⊢ (f = F \land y = A) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
21	20	ralbidv	$⊢ (f = F \land y = A) \to (\forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
22	10 21	anbi12d	$⊢ (f = F \land y = A) \to ((y \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x)) \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)))$
23		df-clim	$⊢ ⇝ = \{⟨f, y⟩ \| (y \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x))\}$
24	22 23	brabga	$⊢ (F \in V \land A \in V) \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)))$
25	24	ex	$⊢ F \in V \to (A \in V \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	1 25	syl	$⊢ φ \to (A \in V \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))))$
27	5 8 26	pm5.21ndd	$⊢ φ \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)))$
28		eluzelz	$⊢ k \in ℤ_{\geq j} \to k \in ℤ$
29	2	eleq1d	$⊢ (φ \land k \in ℤ) \to (F (k) \in ℂ \leftrightarrow B \in ℂ)$
30	2	fvoveq1d	$⊢ (φ \land k \in ℤ) \to \|F (k) - A\| = \|B - A\|$
31	30	breq1d	$⊢ (φ \land k \in ℤ) \to (\|F (k) - A\| < x \leftrightarrow \|B - A\| < x)$
32	29 31	anbi12d	$⊢ (φ \land k \in ℤ) \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
33	28 32	sylan2	$⊢ (φ \land k \in ℤ_{\geq j}) \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
34	33	ralbidva	$⊢ φ \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
35	34	rexbidv	$⊢ φ \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} (B \in ℂ \land \|B - A\| < x))$
36	35	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
37	36	anbi2d	$⊢ φ \to ((A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)))$
38	27 37	bitrd	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)))$

Metamath Proof Explorer

Theorem clim

Proof