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

Theorem rlimcl 13579
Description: Closure of the limit of a sequence of complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
rlimcl  |-  ( F  ~~> r  A  ->  A  e.  CC )

Proof of Theorem rlimcl
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rlimf 13577 . . . 4  |-  ( F  ~~> r  A  ->  F : dom  F --> CC )
2 rlimss 13578 . . . 4  |-  ( F  ~~> r  A  ->  dom  F 
C_  RR )
3 eqidd 2454 . . . 4  |-  ( ( F  ~~> r  A  /\  x  e.  dom  F )  ->  ( F `  x )  =  ( F `  x ) )
41, 2, 3rlim 13571 . . 3  |-  ( F  ~~> r  A  ->  ( F 
~~> r  A  <->  ( A  e.  CC  /\  A. y  e.  RR+  E. z  e.  RR  A. x  e. 
dom  F ( z  <_  x  ->  ( abs `  ( ( F `
 x )  -  A ) )  < 
y ) ) ) )
54ibi 245 . 2  |-  ( F  ~~> r  A  ->  ( A  e.  CC  /\  A. y  e.  RR+  E. z  e.  RR  A. x  e. 
dom  F ( z  <_  x  ->  ( abs `  ( ( F `
 x )  -  A ) )  < 
y ) ) )
65simpld 461 1  |-  ( F  ~~> r  A  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1889   A.wral 2739   E.wrex 2740   class class class wbr 4405   dom cdm 4837   ` cfv 5585  (class class class)co 6295   CCcc 9542   RRcr 9543    < clt 9680    <_ cle 9681    - cmin 9865   RR+crp 11309   abscabs 13309    ~~> r crli 13561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-cnex 9600  ax-resscn 9601
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-pm 7480  df-rlim 13565
This theorem is referenced by:  rlimi  13589  rlimclim1  13621  rlimuni  13626  rlimresb  13641  rlimcld2  13654  rlimabs  13684  rlimcj  13685  rlimre  13686  rlimim  13687  rlimo1  13692  rlimadd  13718  rlimsub  13719  rlimmul  13720  rlimdiv  13721  rlimsqzlem  13724  fsumrlim  13883  dchrisum0lem2a  24367  mulog2sumlem2  24385  mulog2sumlem3  24386
  Copyright terms: Public domain W3C validator