Metamath Proof Explorer

Definition 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 e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cli 
 |-  ~~>
1 vf 
 |-  f
2 vy 
 |-  y
3 2 cv 
 |-  y
4 cc 
 |-  CC
5 3 4 wcel 
 |-  y e. CC
6 vx 
 |-  x
7 crp 
 |-  RR+
8 vj 
 |-  j
9 cz 
 |-  ZZ
10 vk 
 |-  k
11 cuz 
 |-  ZZ>=
12 8 cv 
 |-  j
13 12 11 cfv 
 |-  ( ZZ>= ` j )
14 1 cv 
 |-  f
15 10 cv 
 |-  k
16 15 14 cfv 
 |-  ( f ` k )
17 16 4 wcel 
 |-  ( f ` k ) e. CC
18 cabs 
 |-  abs
19 cmin 
 |-  -
20 16 3 19 co 
 |-  ( ( f ` k ) - y )
21 20 18 cfv 
 |-  ( abs ` ( ( f ` k ) - y ) )
22 clt 
 |-  <
23 6 cv 
 |-  x
24 21 23 22 wbr 
 |-  ( abs ` ( ( f ` k ) - y ) ) < x
25 17 24 wa 
 |-  ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x )
26 25 10 13 wral 
 |-  A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x )
27 26 8 9 wrex 
 |-  E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x )
28 27 6 7 wral 
 |-  A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x )
29 5 28 wa 
 |-  ( 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 ) )
30 29 1 2 copab 
 |-  { <. 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 ) ) }
31 0 30 wceq 
 |-  ~~> = { <. 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 ) ) }