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

Definition df-clim 11962
Description: Define the limit relation for complex number sequences. See clim 11968 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 11958 . 2  class  ~~>
2 vy . . . . . 6  set  y
32cv 1622 . . . . 5  class  y
4 cc 8735 . . . . 5  class  CC
53, 4wcel 1684 . . . 4  wff  y  e.  CC
6 vk . . . . . . . . . . 11  set  k
76cv 1622 . . . . . . . . . 10  class  k
8 vf . . . . . . . . . . 11  set  f
98cv 1622 . . . . . . . . . 10  class  f
107, 9cfv 5255 . . . . . . . . 9  class  ( f `
 k )
1110, 4wcel 1684 . . . . . . . 8  wff  ( f `
 k )  e.  CC
12 cmin 9037 . . . . . . . . . . 11  class  -
1310, 3, 12co 5858 . . . . . . . . . 10  class  ( ( f `  k )  -  y )
14 cabs 11719 . . . . . . . . . 10  class  abs
1513, 14cfv 5255 . . . . . . . . 9  class  ( abs `  ( ( f `  k )  -  y
) )
16 vx . . . . . . . . . 10  set  x
1716cv 1622 . . . . . . . . 9  class  x
18 clt 8867 . . . . . . . . 9  class  <
1915, 17, 18wbr 4023 . . . . . . . 8  wff  ( abs `  ( ( f `  k )  -  y
) )  <  x
2011, 19wa 358 . . . . . . 7  wff  ( ( f `  k )  e.  CC  /\  ( abs `  ( ( f `
 k )  -  y ) )  < 
x )
21 vj . . . . . . . . 9  set  j
2221cv 1622 . . . . . . . 8  class  j
23 cuz 10230 . . . . . . . 8  class  ZZ>=
2422, 23cfv 5255 . . . . . . 7  class  ( ZZ>= `  j )
2520, 6, 24wral 2543 . . . . . 6  wff  A. k  e.  ( ZZ>= `  j )
( ( f `  k )  e.  CC  /\  ( abs `  (
( f `  k
)  -  y ) )  <  x )
26 cz 10024 . . . . . 6  class  ZZ
2725, 21, 26wrex 2544 . . . . 5  wff  E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j )
( ( f `  k )  e.  CC  /\  ( abs `  (
( f `  k
)  -  y ) )  <  x )
28 crp 10354 . . . . 5  class  RR+
2927, 16, 28wral 2543 . . . 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 358 . . 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 4076 . 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 1623 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  11966  clim  11968
  Copyright terms: Public domain W3C validator