Definition df-clim 8235

Description: Define the limit relation for complex number sequences. See clim 8237 for its relational expression.

Assertion

Ref	Expression
df-clim	|- ~~> = {<.f, y>. | (y e. CC /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((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 8234	. 2 class ~~>
2		vy	. . . . . 6 set y
3	2	cv 1297	. . . . 5 class y
4		cc 6384	. . . . 5 class CC
5	3, 4	wcel 1300	. . . 4 wff y e. CC
6		cc0 6386	. . . . . . 7 class 0
7		vx	. . . . . . . 8 set x
8	7	cv 1297	. . . . . . 7 class x
9		clt 6653	. . . . . . 7 class <
10	6, 8, 9	wbr 3338	. . . . . 6 wff 0 < x
11		vj	. . . . . . . . . . 11 set j
12	11	cv 1297	. . . . . . . . . 10 class j
13		vk	. . . . . . . . . . 11 set k
14	13	cv 1297	. . . . . . . . . 10 class k
15		cle 6448	. . . . . . . . . 10 class <_
16	12, 14, 15	wbr 3338	. . . . . . . . 9 wff j <_ k
17		vf	. . . . . . . . . . . . 13 set f
18	17	cv 1297	. . . . . . . . . . . 12 class f
19	14, 18	cfv 3998	. . . . . . . . . . 11 class (f` k)
20	19, 4	wcel 1300	. . . . . . . . . 10 wff (f` k) e. CC
21		cmin 6445	. . . . . . . . . . . . 13 class -
22	19, 3, 21	co 4884	. . . . . . . . . . . 12 class ((f` k) - y)
23		cabs 8000	. . . . . . . . . . . 12 class abs
24	22, 23	cfv 3998	. . . . . . . . . . 11 class (abs` ((f` k) - y))
25	24, 8, 9	wbr 3338	. . . . . . . . . 10 wff (abs` ((f` k) - y)) < x
26	20, 25	wa 240	. . . . . . . . 9 wff ((f` k) e. CC /\ (abs` ((f` k) - y)) < x)
27	16, 26	wi 3	. . . . . . . 8 wff (j <_ k -> ((f` k) e. CC /\ (abs` ((f` k) - y)) < x))
28		cz 6451	. . . . . . . 8 class ZZ
29	27, 13, 28	wral 2105	. . . . . . 7 wff A.k e. ZZ (j <_ k -> ((f` k) e. CC /\ (abs` ((f` k) - y)) < x))
30	29, 11, 28	wrex 2106	. . . . . 6 wff E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. CC /\ (abs` ((f` k) - y)) < x))
31	10, 30	wi 3	. . . . 5 wff (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. CC /\ (abs` ((f` k) - y)) < x)))
32		cr 6385	. . . . 5 class RR
33	31, 7, 32	wral 2105	. . . 4 wff A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. CC /\ (abs` ((f` k) - y)) < x)))
34	5, 33	wa 240	. . 3 wff (y e. CC /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. CC /\ (abs` ((f` k) - y)) < x))))
35	34, 17, 2	copab 3395	. 2 class {<.f, y>. | (y e. CC /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. CC /\ (abs` ((f` k) - y)) < x))))}
36	1, 35	wceq 1298	1 wff ~~> = {<.f, y>. | (y e. CC /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. CC /\ (abs` ((f` k) - y)) < x))))}

This definition is referenced by:  climrel 8236  clim 8237

Copyright terms: Public domain