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 ) ) }