MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  climrel Structured version   Unicode version

Theorem climrel 13340
Description: The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
Assertion
Ref Expression
climrel  |-  Rel  ~~>

Proof of Theorem climrel
Dummy variables  j 
k  x  y  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-clim 13336 . 2  |-  ~~>  =  { <. 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 ) ) }
21relopabi 5057 1  |-  Rel  ~~>
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367    e. wcel 1836   A.wral 2746   E.wrex 2747   class class class wbr 4384   Rel wrel 4935   ` cfv 5513  (class class class)co 6218   CCcc 9423    < clt 9561    - cmin 9740   ZZcz 10803   ZZ>=cuz 11023   RR+crp 11161   abscabs 13092    ~~> cli 13332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pr 4618
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rex 2752  df-rab 2755  df-v 3053  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-sn 3962  df-pr 3964  df-op 3968  df-opab 4443  df-xp 4936  df-rel 4937  df-clim 13336
This theorem is referenced by:  clim  13342  climcl  13347  climi  13358  climrlim2  13395  fclim  13401  climrecl  13431  climge0  13432  iserex  13504  caurcvg2  13525  caucvg  13526  iseralt  13532  fsumcvg3  13576  cvgcmpce  13657  climfsum  13659  climcnds  13688  trirecip  13699  ntrivcvgn0  13732  ovoliunlem1  22021  mbflimlem  22182  abelthlem5  22938  emcllem6  23470  lgamgulmlem4  28803  binomcxplemnn0  31462  binomcxplemnotnn0  31469  climf  31833  sumnnodd  31841  ioodvbdlimc1lem2  31934  ioodvbdlimc2lem  31936  stirlinglem12  32072  fouriersw  32219
  Copyright terms: Public domain W3C validator