MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-clim Unicode version

Definition df-clim 11958
Description: Define the limit relation for complex number sequences. See clim 11964 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
StepHypRef Expression
1 cli 11954 . 2  class  ~~>
2 vy . . . . . 6  set  y
32cv 1624 . . . . 5  class  y
4 cc 8732 . . . . 5  class  CC
53, 4wcel 1687 . . . 4  wff  y  e.  CC
6 vk . . . . . . . . . . 11  set  k
76cv 1624 . . . . . . . . . 10  class  k
8 vf . . . . . . . . . . 11  set  f
98cv 1624 . . . . . . . . . 10  class  f
107, 9cfv 5223 . . . . . . . . 9  class  ( f `
 k )
1110, 4wcel 1687 . . . . . . . 8  wff  ( f `
 k )  e.  CC
12 cmin 9034 . . . . . . . . . . 11  class  -
1310, 3, 12co 5821 . . . . . . . . . 10  class  ( ( f `  k )  -  y )
14 cabs 11715 . . . . . . . . . 10  class  abs
1513, 14cfv 5223 . . . . . . . . 9  class  ( abs `  ( ( f `  k )  -  y
) )
16 vx . . . . . . . . . 10  set  x
1716cv 1624 . . . . . . . . 9  class  x
18 clt 8864 . . . . . . . . 9  class  <
1915, 17, 18wbr 4026 . . . . . . . 8  wff  ( abs `  ( ( f `  k )  -  y
) )  <  x
2011, 19wa 360 . . . . . . 7  wff  ( ( f `  k )  e.  CC  /\  ( abs `  ( ( f `
 k )  -  y ) )  < 
x )
21 vj . . . . . . . . 9  set  j
2221cv 1624 . . . . . . . 8  class  j
23 cuz 10227 . . . . . . . 8  class  ZZ>=
2422, 23cfv 5223 . . . . . . 7  class  ( ZZ>= `  j )
2520, 6, 24wral 2546 . . . . . 6  wff  A. k  e.  ( ZZ>= `  j )
( ( f `  k )  e.  CC  /\  ( abs `  (
( f `  k
)  -  y ) )  <  x )
26 cz 10021 . . . . . 6  class  ZZ
2725, 21, 26wrex 2547 . . . . 5  wff  E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j )
( ( f `  k )  e.  CC  /\  ( abs `  (
( f `  k
)  -  y ) )  <  x )
28 crp 10351 . . . . 5  class  RR+
2927, 16, 28wral 2546 . . . 4  wff  A. x  e.  RR+  E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j )
( ( f `  k )  e.  CC  /\  ( abs `  (
( f `  k
)  -  y ) )  <  x )
305, 29wa 360 . . 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 ) )
3130, 8, 2copab 4079 . 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 ) ) }
321, 31wceq 1625 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 ) ) }
Colors of variables: wff set class
This definition is referenced by:  climrel  11962  clim  11964
  Copyright terms: Public domain W3C validator