df-clim

Description: Define the limit relation for complex number sequences. See clim for its relational expression. (Contributed by NM, 28-Aug-2005)

		Ref	Expression
	Assertion	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))\}$

Step	Hyp	Ref	Expression
0		cli	$class ⇝$
1		vf	$setvar f$
2		vy	$setvar y$
3	2	cv	$setvar y$
4		cc	$class ℂ$
5	3 4	wcel	$wff y \in ℂ$
6		vx	$setvar x$
7		crp	$class ℝ^{+}$
8		vj	$setvar j$
9		cz	$class ℤ$
10		vk	$setvar k$
11		cuz	$class ℤ_{\geq}$
12	8	cv	$setvar j$
13	12 11	cfv	$class ℤ_{\geq j}$
14	1	cv	$setvar f$
15	10	cv	$setvar k$
16	15 14	cfv	$class f (k)$
17	16 4	wcel	$wff f (k) \in ℂ$
18		cabs	$class abs$
19		cmin	$class -$
20	16 3 19	co	$class (f (k) - y)$
21	20 18	cfv	$class \|f (k) - y\|$
22		clt	$class <$
23	6	cv	$setvar x$
24	21 23 22	wbr	$wff \|f (k) - y\| < x$
25	17 24	wa	$wff (f (k) \in ℂ \land \|f (k) - y\| < x)$
26	25 10 13	wral	$wff \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x)$
27	26 8 9	wrex	$wff \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x)$
28	27 6 7	wral	$wff \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x)$
29	5 28	wa	$wff (y \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x))$
30	29 1 2	copab	$class \{⟨f, y⟩ \| (y \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x))\}$
31	0 30	wceq	$wff ⇝ = \{⟨f, y⟩ \| (y \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x))\}$

Metamath Proof Explorer