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

Theorem climrel 15528
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 𝑗 𝑘 𝑥 𝑦 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-clim 15524 . 2 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
21relopabiv 5830 1 Rel ⇝
Colors of variables: wff setvar class
Syntax hints:  wa 395  wcel 2108  wral 3061  wrex 3070   class class class wbr 5143  Rel wrel 5690  cfv 6561  (class class class)co 7431  cc 11153   < clt 11295  cmin 11492  cz 12613  cuz 12878  +crp 13034  abscabs 15273  cli 15520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692  df-clim 15524
This theorem is referenced by:  clim  15530  climcl  15535  climi  15546  climrlim2  15583  fclim  15589  climrecl  15619  climge0  15620  iserex  15693  caurcvg2  15714  caucvg  15715  iseralt  15721  fsumcvg3  15765  cvgcmpce  15854  climfsum  15856  climcnds  15887  trirecip  15899  ntrivcvgn0  15934  ovoliunlem1  25537  mbflimlem  25702  abelthlem5  26479  emcllem6  27044  lgamgulmlem4  27075  binomcxplemnn0  44368  binomcxplemnotnn0  44375  climf  45637  sumnnodd  45645  climf2  45681  climd  45687  clim2d  45688  climfv  45706  climuzlem  45758  climlimsup  45775  climlimsupcex  45784  climliminflimsupd  45816  climliminf  45821  liminflimsupclim  45822  xlimclimdm  45869  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stirlinglem12  46100  fouriersw  46246
  Copyright terms: Public domain W3C validator