Definition df-clim 14219

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

Assertion

Ref	Expression
df-clim	|- ~~> = { <. f , y >. | ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) }

Distinct variable group:   j, k, x, y, f

Detailed syntax breakdown of Definition df-clim

Step	Hyp	Ref	Expression
1		cli 14215	. 2 class ~~>
2		vy	. . . . . 6 setvar y
3	2	cv 1482	. . . . 5 class y
4		cc 9934	. . . . 5 class CC
5	3, 4	wcel 1990	. . . 4 wff y e. CC
6		vk	. . . . . . . . . . 11 setvar k
7	6	cv 1482	. . . . . . . . . 10 class k
8		vf	. . . . . . . . . . 11 setvar f
9	8	cv 1482	. . . . . . . . . 10 class f
10	7, 9	cfv 5888	. . . . . . . . 9 class ( f ` k )
11	10, 4	wcel 1990	. . . . . . . 8 wff ( f ` k ) e. CC
12		cmin 10266	. . . . . . . . . . 11 class -
13	10, 3, 12	co 6650	. . . . . . . . . 10 class ( ( f ` k ) - y )
14		cabs 13974	. . . . . . . . . 10 class abs
15	13, 14	cfv 5888	. . . . . . . . 9 class ( abs ` ( ( f ` k ) - y ) )
16		vx	. . . . . . . . . 10 setvar x
17	16	cv 1482	. . . . . . . . 9 class x
18		clt 10074	. . . . . . . . 9 class <
19	15, 17, 18	wbr 4653	. . . . . . . 8 wff ( abs ` ( ( f ` k ) - y ) ) < x
20	11, 19	wa 384	. . . . . . 7 wff ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x )
21		vj	. . . . . . . . 9 setvar j
22	21	cv 1482	. . . . . . . 8 class j
23		cuz 11687	. . . . . . . 8 class ZZ>=
24	22, 23	cfv 5888	. . . . . . 7 class ( ZZ>= ` j )
25	20, 6, 24	wral 2912	. . . . . 6 wff A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x )
26		cz 11377	. . . . . 6 class ZZ
27	25, 21, 26	wrex 2913	. . . . 5 wff E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x )
28		crp 11832	. . . . 5 class RR+
29	27, 16, 28	wral 2912	. . . 4 wff A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x )
30	5, 29	wa 384	. . 3 wff ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) )
31	30, 8, 2	copab 4712	. 2 class { <. f , y >. | ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) }
32	1, 31	wceq 1483	1 wff ~~> = { <. f , y >. | ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) }

This definition is referenced by:  climrel  14223  clim  14225  climf  39854  climf2  39898