HomeHome Intuitionistic Logic Explorer
Theorem List (p. 101 of 106)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 10001-10100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremabsltd 10001 Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   =>    |-  ( ph  ->  ( ( abs `  A )  <  B  <->  ( -u B  <  A  /\  A  <  B ) ) )
 
Theoremabsled 10002 Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   =>    |-  ( ph  ->  ( ( abs `  A )  <_  B  <->  ( -u B  <_  A  /\  A  <_  B ) ) )
 
Theoremabssubge0d 10003 Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   =>    |-  ( ph  ->  ( abs `  ( B  -  A ) )  =  ( B  -  A ) )
 
Theoremabssuble0d 10004 Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   =>    |-  ( ph  ->  ( abs `  ( A  -  B ) )  =  ( B  -  A ) )
 
Theoremabsdifltd 10005 The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR )   =>    |-  ( ph  ->  (
 ( abs `  ( A  -  B ) )  <  C 
 <->  ( ( B  -  C )  <  A  /\  A  <  ( B  +  C ) ) ) )
 
Theoremabsdifled 10006 The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR )   =>    |-  ( ph  ->  (
 ( abs `  ( A  -  B ) )  <_  C 
 <->  ( ( B  -  C )  <_  A  /\  A  <_  ( B  +  C ) ) ) )
 
Theoremicodiamlt 10007 Two elements in a half-open interval have separation strictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014.)
 |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e.  ( A [,) B )  /\  D  e.  ( A [,) B ) ) )  ->  ( abs `  ( C  -  D ) )  < 
 ( B  -  A ) )
 
Theoremabscld 10008 Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  ( abs `  A )  e. 
 RR )
 
Theoremabsvalsqd 10009 Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  (
 ( abs `  A ) ^ 2 )  =  ( A  x.  ( * `  A ) ) )
 
Theoremabsvalsq2d 10010 Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  (
 ( abs `  A ) ^ 2 )  =  ( ( ( Re
 `  A ) ^
 2 )  +  (
 ( Im `  A ) ^ 2 ) ) )
 
Theoremabsge0d 10011 Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  0  <_  ( abs `  A ) )
 
Theoremabsval2d 10012 Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  ( abs `  A )  =  ( sqr `  (
 ( ( Re `  A ) ^ 2
 )  +  ( ( Im `  A ) ^ 2 ) ) ) )
 
Theoremabs00d 10013 The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  ( abs `  A )  =  0 )   =>    |-  ( ph  ->  A  =  0 )
 
Theoremabsne0d 10014 The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A  =/=  0 )   =>    |-  ( ph  ->  ( abs `  A )  =/=  0 )
 
Theoremabsrpclapd 10015 The absolute value of a complex number apart from zero is a positive real. (Contributed by Jim Kingdon, 13-Aug-2021.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A #  0 )   =>    |-  ( ph  ->  ( abs `  A )  e.  RR+ )
 
Theoremabsnegd 10016 Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  ( abs `  -u A )  =  ( abs `  A ) )
 
Theoremabscjd 10017 The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  ( abs `  ( * `  A ) )  =  ( abs `  A ) )
 
Theoremreleabsd 10018 The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  ( Re `  A )  <_  ( abs `  A )
 )
 
Theoremabsexpd 10019 Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  N  e.  NN0 )   =>    |-  ( ph  ->  ( abs `  ( A ^ N ) )  =  ( ( abs `  A ) ^ N ) )
 
Theoremabssubd 10020 Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  ( abs `  ( A  -  B ) )  =  ( abs `  ( B  -  A ) ) )
 
Theoremabsmuld 10021 Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  ( abs `  ( A  x.  B ) )  =  ( ( abs `  A )  x.  ( abs `  B ) ) )
 
Theoremabsdivapd 10022 Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  B #  0 )   =>    |-  ( ph  ->  ( abs `  ( A  /  B ) )  =  ( ( abs `  A )  /  ( abs `  B ) ) )
 
Theoremabstrid 10023 Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  ( abs `  ( A  +  B ) )  <_  ( ( abs `  A )  +  ( abs `  B ) ) )
 
Theoremabs2difd 10024 Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  ( ( abs `  A )  -  ( abs `  B ) )  <_  ( abs `  ( A  -  B ) ) )
 
Theoremabs2dif2d 10025 Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  ( abs `  ( A  -  B ) )  <_  ( ( abs `  A )  +  ( abs `  B ) ) )
 
Theoremabs2difabsd 10026 Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  ( abs `  ( ( abs `  A )  -  ( abs `  B )
 ) )  <_  ( abs `  ( A  -  B ) ) )
 
Theoremabs3difd 10027 Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   =>    |-  ( ph  ->  ( abs `  ( A  -  B ) )  <_  ( ( abs `  ( A  -  C ) )  +  ( abs `  ( C  -  B ) ) ) )
 
Theoremabs3lemd 10028 Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  RR )   &    |-  ( ph  ->  ( abs `  ( A  -  C ) )  < 
 ( D  /  2
 ) )   &    |-  ( ph  ->  ( abs `  ( C  -  B ) )  < 
 ( D  /  2
 ) )   =>    |-  ( ph  ->  ( abs `  ( A  -  B ) )  <  D )
 
Theoremqdenre 10029* The rational numbers are dense in 
RR: any real number can be approximated with arbitrary precision by a rational number. For order theoretic density, see qbtwnre 9213. (Contributed by BJ, 15-Oct-2021.)
 |-  ( ( A  e.  RR  /\  B  e.  RR+ )  ->  E. x  e.  QQ  ( abs `  ( x  -  A ) )  <  B )
 
3.8  Elementary limits and convergence
 
3.8.1  Limits
 
Syntaxcli 10030 Extend class notation with convergence relation for limits.
 class  ~~>
 
Definitiondf-clim 10031* Define the limit relation for complex number sequences. See clim 10033 for its relational expression. (Contributed by NM, 28-Aug-2005.)
 |-  ~~>  =  { <. 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 ) ) }
 
Theoremclimrel 10032 The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |- 
 Rel 
 ~~>
 
Theoremclim 10033* Express the predicate: The limit of complex number sequence  F is  A, or  F converges to  A. This means that for any real  x, no matter how small, there always exists an integer 
j such that the absolute difference of any later complex number in the sequence and the limit is less than  x. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
 |-  ( ph  ->  F  e.  V )   &    |-  ( ( ph  /\  k  e.  ZZ )  ->  ( F `  k
 )  =  B )   =>    |-  ( ph  ->  ( F  ~~>  A 
 <->  ( A  e.  CC  /\ 
 A. x  e.  RR+  E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j ) ( B  e.  CC  /\  ( abs `  ( B  -  A ) )  < 
 x ) ) ) )
 
Theoremclimcl 10034 Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
 |-  ( F  ~~>  A  ->  A  e.  CC )
 
Theoremclim2 10035* Express the predicate: The limit of complex number sequence  F is  A, or  F converges to  A, with more general quantifier restrictions than clim 10033. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  e.  V )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  B )   =>    |-  ( ph  ->  ( F 
 ~~>  A  <->  ( A  e.  CC  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ( B  e.  CC  /\  ( abs `  ( B  -  A ) )  < 
 x ) ) ) )
 
Theoremclim2c 10036* Express the predicate  F converges to  A. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  e.  V )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  B )   &    |-  ( ph  ->  A  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  B  e.  CC )   =>    |-  ( ph  ->  ( F 
 ~~>  A  <->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ( abs `  ( B  -  A ) )  <  x ) )
 
Theoremclim0 10037* Express the predicate  F converges to  0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  e.  V )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  B )   =>    |-  ( ph  ->  ( F 
 ~~>  0  <->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ( B  e.  CC  /\  ( abs `  B )  < 
 x ) ) )
 
Theoremclim0c 10038* Express the predicate  F converges to  0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  e.  V )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  B )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  B  e.  CC )   =>    |-  ( ph  ->  ( F  ~~>  0  <->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ( abs `  B )  <  x ) )
 
Theoremclimi 10039* Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  B )   &    |-  ( ph  ->  F  ~~>  A )   =>    |-  ( ph  ->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
 ( B  e.  CC  /\  ( abs `  ( B  -  A ) )  <  C ) )
 
Theoremclimi2 10040* Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  B )   &    |-  ( ph  ->  F  ~~>  A )   =>    |-  ( ph  ->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
 ( abs `  ( B  -  A ) )  <  C )
 
Theoremclimi0 10041* Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  B )   &    |-  ( ph  ->  F  ~~>  0 )   =>    |-  ( ph  ->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
 ( abs `  B )  <  C )
 
Theoremclimconst 10042* An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  e.  V )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  =  A )   =>    |-  ( ph  ->  F  ~~>  A )
 
Theoremclimconst2 10043 A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  ( ZZ>= `  M )  C_  Z   &    |-  Z  e.  _V   =>    |-  (
 ( A  e.  CC  /\  M  e.  ZZ )  ->  ( Z  X.  { A } )  ~~>  A )
 
Theoremclimz 10044 The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  ( ZZ  X.  {
 0 } )  ~~>  0
 
Theoremclimuni 10045 An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
 |-  ( ( F  ~~>  A  /\  F 
 ~~>  B )  ->  A  =  B )
 
Theoremfclim 10046 The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
 |-  ~~>  : dom  ~~>  --> CC
 
Theoremclimdm 10047 Two ways to express that a function has a limit. (The expression  (  ~~>  `  F
) is sometimes useful as a shorthand for "the unique limit of the function  F"). (Contributed by Mario Carneiro, 18-Mar-2014.)
 |-  ( F  e.  dom  ~~>  <->  F  ~~>  ( 
 ~~>  `  F ) )
 
Theoremclimeu 10048* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
 |-  ( F  ~~>  A  ->  E! x  F  ~~>  x )
 
Theoremclimreu 10049* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
 |-  ( F  ~~>  A  ->  E! x  e.  CC  F  ~~>  x )
 
Theoremclimmo 10050* An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)
 |- 
 E* x  F  ~~>  x
 
Theoremclimeq 10051* Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  F  e.  V )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  =  ( G `
  k ) )   =>    |-  ( ph  ->  ( F  ~~>  A 
 <->  G  ~~>  A ) )
 
Theoremclimmpt 10052* Exhibit a function  G with the same convergence properties as the not-quite-function  F. (Contributed by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  G  =  ( k  e.  Z  |->  ( F `  k ) )   =>    |-  ( ( M  e.  ZZ  /\  F  e.  V )  ->  ( F  ~~>  A  <->  G  ~~>  A ) )
 
Theorem2clim 10053* If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  G  e.  V )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( G `  k )  e. 
 CC )   &    |-  ( ph  ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
 ( abs `  ( ( F `  k )  -  ( G `  k ) ) )  <  x )   &    |-  ( ph  ->  F  ~~>  A )   =>    |-  ( ph  ->  G  ~~>  A )
 
Theoremclimshftlemg 10054 A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)
 |-  ( ( M  e.  ZZ  /\  F  e.  V )  ->  ( F  ~~>  A  ->  ( F  shift  M )  ~~>  A )
 )
 
Theoremclimres 10055 A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  ( ( M  e.  ZZ  /\  F  e.  V )  ->  ( ( F  |`  ( ZZ>= `  M )
 )  ~~>  A  <->  F  ~~>  A ) )
 
Theoremclimshft 10056 A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  ( ( M  e.  ZZ  /\  F  e.  V )  ->  ( ( F 
 shift  M )  ~~>  A  <->  F  ~~>  A ) )
 
Theoremiserclim0 10057 The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.)
 |-  ( M  e.  ZZ  ->  seq M (  +  ,  ( ( ZZ>= `  M )  X.  { 0 } ) ,  CC )  ~~>  0 )
 
Theoremclimshft2 10058* A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  K  e.  ZZ )   &    |-  ( ph  ->  F  e.  W )   &    |-  ( ph  ->  G  e.  X )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  ( k  +  K ) )  =  ( F `  k
 ) )   =>    |-  ( ph  ->  ( F 
 ~~>  A  <->  G  ~~>  A ) )
 
Theoremclimabs0 10059* Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  e.  V )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  =  ( abs `  ( F `  k ) ) )   =>    |-  ( ph  ->  ( F 
 ~~>  0  <->  G  ~~>  0 ) )
 
Theoremclimcn1 10060* Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  A  e.  B )   &    |-  ( ( ph  /\  z  e.  B )  ->  ( F `  z )  e. 
 CC )   &    |-  ( ph  ->  G  ~~>  A )   &    |-  ( ph  ->  H  e.  W )   &    |-  (
 ( ph  /\  x  e.  RR+ )  ->  E. y  e.  RR+  A. z  e.  B  ( ( abs `  (
 z  -  A ) )  <  y  ->  ( abs `  ( ( F `  z )  -  ( F `  A ) ) )  <  x ) )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  e.  B )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( H `  k )  =  ( F `  ( G `  k ) ) )   =>    |-  ( ph  ->  H  ~~>  ( F `  A ) )
 
Theoremclimcn2 10061* Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  A  e.  C )   &    |-  ( ph  ->  B  e.  D )   &    |-  ( ( ph  /\  ( u  e.  C  /\  v  e.  D ) )  ->  ( u F v )  e. 
 CC )   &    |-  ( ph  ->  G  ~~>  A )   &    |-  ( ph  ->  H  ~~>  B )   &    |-  ( ph  ->  K  e.  W )   &    |-  (
 ( ph  /\  x  e.  RR+ )  ->  E. y  e.  RR+  E. z  e.  RR+  A. u  e.  C  A. v  e.  D  ( ( ( abs `  ( u  -  A ) )  <  y  /\  ( abs `  ( v  -  B ) )  < 
 z )  ->  ( abs `  ( ( u F v )  -  ( A F B ) ) )  <  x ) )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  e.  C )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( H `  k )  e.  D )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( K `  k
 )  =  ( ( G `  k ) F ( H `  k ) ) )   =>    |-  ( ph  ->  K  ~~>  ( A F B ) )
 
Theoremaddcn2 10062* Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (We write out the definition directly because df-cn and df-cncf are not yet available to us. See addcn for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.)
 |-  ( ( A  e.  RR+  /\  B  e.  CC  /\  C  e.  CC )  ->  E. y  e.  RR+  E. z  e.  RR+  A. u  e.  CC  A. v  e. 
 CC  ( ( ( abs `  ( u  -  B ) )  < 
 y  /\  ( abs `  ( v  -  C ) )  <  z ) 
 ->  ( abs `  (
 ( u  +  v
 )  -  ( B  +  C ) ) )  <  A ) )
 
Theoremsubcn2 10063* Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
 |-  ( ( A  e.  RR+  /\  B  e.  CC  /\  C  e.  CC )  ->  E. y  e.  RR+  E. z  e.  RR+  A. u  e.  CC  A. v  e. 
 CC  ( ( ( abs `  ( u  -  B ) )  < 
 y  /\  ( abs `  ( v  -  C ) )  <  z ) 
 ->  ( abs `  (
 ( u  -  v
 )  -  ( B  -  C ) ) )  <  A ) )
 
Theoremmulcn2 10064* Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
 |-  ( ( A  e.  RR+  /\  B  e.  CC  /\  C  e.  CC )  ->  E. y  e.  RR+  E. z  e.  RR+  A. u  e.  CC  A. v  e. 
 CC  ( ( ( abs `  ( u  -  B ) )  < 
 y  /\  ( abs `  ( v  -  C ) )  <  z ) 
 ->  ( abs `  (
 ( u  x.  v
 )  -  ( B  x.  C ) ) )  <  A ) )
 
Theoremcn1lem 10065* A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
 |-  F : CC --> CC   &    |-  (
 ( z  e.  CC  /\  A  e.  CC )  ->  ( abs `  (
 ( F `  z
 )  -  ( F `
  A ) ) )  <_  ( abs `  ( z  -  A ) ) )   =>    |-  ( ( A  e.  CC  /\  x  e.  RR+ )  ->  E. y  e.  RR+  A. z  e.  CC  ( ( abs `  (
 z  -  A ) )  <  y  ->  ( abs `  ( ( F `  z )  -  ( F `  A ) ) )  <  x ) )
 
Theoremabscn2 10066* The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
 |-  ( ( A  e.  CC  /\  x  e.  RR+ )  ->  E. y  e.  RR+  A. z  e.  CC  (
 ( abs `  ( z  -  A ) )  < 
 y  ->  ( abs `  ( ( abs `  z
 )  -  ( abs `  A ) ) )  <  x ) )
 
Theoremcjcn2 10067* The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
 |-  ( ( A  e.  CC  /\  x  e.  RR+ )  ->  E. y  e.  RR+  A. z  e.  CC  (
 ( abs `  ( z  -  A ) )  < 
 y  ->  ( abs `  ( ( * `  z )  -  ( * `  A ) ) )  <  x ) )
 
Theoremrecn2 10068* The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
 |-  ( ( A  e.  CC  /\  x  e.  RR+ )  ->  E. y  e.  RR+  A. z  e.  CC  (
 ( abs `  ( z  -  A ) )  < 
 y  ->  ( abs `  ( ( Re `  z )  -  ( Re `  A ) ) )  <  x ) )
 
Theoremimcn2 10069* The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
 |-  ( ( A  e.  CC  /\  x  e.  RR+ )  ->  E. y  e.  RR+  A. z  e.  CC  (
 ( abs `  ( z  -  A ) )  < 
 y  ->  ( abs `  ( ( Im `  z )  -  ( Im `  A ) ) )  <  x ) )
 
Theoremclimcn1lem 10070* The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  H : CC --> CC   &    |-  ( ( A  e.  CC  /\  x  e.  RR+ )  ->  E. y  e.  RR+  A. z  e.  CC  (
 ( abs `  ( z  -  A ) )  < 
 y  ->  ( abs `  ( ( H `  z )  -  ( H `  A ) ) )  <  x ) )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  =  ( H `
  ( F `  k ) ) )   =>    |-  ( ph  ->  G  ~~>  ( H `  A ) )
 
Theoremclimabs 10071* Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  =  ( abs `  ( F `  k
 ) ) )   =>    |-  ( ph  ->  G  ~~>  ( abs `  A )
 )
 
Theoremclimcj 10072* Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  =  ( * `
  ( F `  k ) ) )   =>    |-  ( ph  ->  G  ~~>  ( * `  A ) )
 
Theoremclimre 10073* Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  =  ( Re
 `  ( F `  k ) ) )   =>    |-  ( ph  ->  G  ~~>  ( Re `  A ) )
 
Theoremclimim 10074* Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  =  ( Im
 `  ( F `  k ) ) )   =>    |-  ( ph  ->  G  ~~>  ( Im `  A ) )
 
Theoremclimrecl 10075* The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 RR )   =>    |-  ( ph  ->  A  e.  RR )
 
Theoremclimge0 10076* A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 RR )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  0  <_  ( F `
  k ) )   =>    |-  ( ph  ->  0  <_  A )
 
Theoremclimadd 10077* Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by NM, 24-Sep-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  H  e.  X )   &    |-  ( ph  ->  G  ~~>  B )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( H `  k
 )  =  ( ( F `  k )  +  ( G `  k ) ) )   =>    |-  ( ph  ->  H  ~~>  ( A  +  B ) )
 
Theoremclimmul 10078* Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by NM, 27-Dec-2005.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  H  e.  X )   &    |-  ( ph  ->  G  ~~>  B )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( H `  k
 )  =  ( ( F `  k )  x.  ( G `  k ) ) )   =>    |-  ( ph  ->  H  ~~>  ( A  x.  B ) )
 
Theoremclimsub 10079* Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  H  e.  X )   &    |-  ( ph  ->  G  ~~>  B )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( H `  k
 )  =  ( ( F `  k )  -  ( G `  k ) ) )   =>    |-  ( ph  ->  H  ~~>  ( A  -  B ) )
 
Theoremclimaddc1 10080* Limit of a constant  C added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  =  ( ( F `  k )  +  C ) )   =>    |-  ( ph  ->  G  ~~>  ( A  +  C ) )
 
Theoremclimaddc2 10081* Limit of a constant  C added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  =  ( C  +  ( F `  k ) ) )   =>    |-  ( ph  ->  G  ~~>  ( C  +  A ) )
 
Theoremclimmulc2 10082* Limit of a sequence multiplied by a constant  C. Corollary 12-2.2 of [Gleason] p. 171. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  =  ( C  x.  ( F `  k ) ) )   =>    |-  ( ph  ->  G  ~~>  ( C  x.  A ) )
 
Theoremclimsubc1 10083* Limit of a constant  C subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  =  ( ( F `  k )  -  C ) )   =>    |-  ( ph  ->  G  ~~>  ( A  -  C ) )
 
Theoremclimsubc2 10084* Limit of a constant  C minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  =  ( C  -  ( F `  k ) ) )   =>    |-  ( ph  ->  G  ~~>  ( C  -  A ) )
 
Theoremclimle 10085* Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  G  ~~>  B )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 RR )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  e.  RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  <_  ( G `  k ) )   =>    |-  ( ph  ->  A  <_  B )
 
Theoremclimsqz 10086* Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 RR )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  e.  RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  <_  ( G `  k ) )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  <_  A )   =>    |-  ( ph  ->  G  ~~>  A )
 
Theoremclimsqz2 10087* Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  G  e.  W )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 RR )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  e.  RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  <_  ( F `  k ) )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  A  <_  ( G `  k ) )   =>    |-  ( ph  ->  G  ~~>  A )
 
Theoremclim2iser 10088* The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  N  e.  Z )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ph  ->  seq
 M (  +  ,  F ,  CC )  ~~>  A )   =>    |-  ( ph  ->  seq ( N  +  1 )
 (  +  ,  F ,  CC )  ~~>  ( A  -  (  seq M (  +  ,  F ,  CC ) `  N ) ) )
 
Theoremclim2iser2 10089* The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  N  e.  Z )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ph  ->  seq ( N  +  1 ) (  +  ,  F ,  CC )  ~~>  A )   =>    |-  ( ph  ->  seq M (  +  ,  F ,  CC )  ~~>  ( A  +  (  seq M (  +  ,  F ,  CC ) `  N ) ) )
 
Theoremiiserex 10090* An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  N  e.  Z )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   =>    |-  ( ph  ->  (  seq M (  +  ,  F ,  CC )  e.  dom  ~~> 
 <-> 
 seq N (  +  ,  F ,  CC )  e.  dom  ~~>  ) )
 
Theoremiisermulc2 10091* Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  seq M (  +  ,  F ,  CC )  ~~>  A )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  =  ( C  x.  ( F `  k ) ) )   =>    |-  ( ph  ->  seq M (  +  ,  G ,  CC )  ~~>  ( C  x.  A ) )
 
Theoremclimlec2 10092* Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  F  ~~>  B )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  A  <_  ( F `  k
 ) )   =>    |-  ( ph  ->  A  <_  B )
 
Theoremiserile 10093* Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  seq M (  +  ,  F ,  CC )  ~~>  A )   &    |-  ( ph  ->  seq
 M (  +  ,  G ,  CC )  ~~>  B )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  e. 
 RR )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  <_  ( G `  k ) )   =>    |-  ( ph  ->  A 
 <_  B )
 
Theoremiserige0 10094* The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  seq M (  +  ,  F ,  CC )  ~~>  A )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  0  <_  ( F `  k
 ) )   =>    |-  ( ph  ->  0  <_  A )
 
Theoremclimub 10095* The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  N  e.  Z )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 RR )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  <_  ( F `  ( k  +  1 ) ) )   =>    |-  ( ph  ->  ( F `  N ) 
 <_  A )
 
Theoremclimserile 10096* The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by Jim Kingdon, 22-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  N  e.  Z )   &    |-  ( ph  ->  seq M (  +  ,  F ,  CC )  ~~>  A )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  0  <_  ( F `  k
 ) )   =>    |-  ( ph  ->  (  seq M (  +  ,  F ,  CC ) `  N )  <_  A )
 
Theoremclimcau 10097* A converging sequence of complex numbers is a Cauchy sequence. The converse would require excluded middle or a different definition of Cauchy sequence (for example, fixing a rate of convergence as in climcvg1n 10100). Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( ( M  e.  ZZ  /\  F  e.  dom  ~~>  ) 
 ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ( abs `  ( ( F `  k )  -  ( F `  j ) ) )  <  x )
 
Theoremclimrecvg1n 10098* A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within  C  /  n of the nth term, where  C is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
 |-  ( ph  ->  F : NN --> RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( abs `  ( ( F `  k )  -  ( F `  n ) ) )  <  ( C  /  n ) )   =>    |-  ( ph  ->  F  e.  dom  ~~>  )
 
Theoremclimcvg1nlem 10099* Lemma for climcvg1n 10100. We construct sequences of the real and imaginary parts of each term of  F, show those converge, and use that to show that  F converges. (Contributed by Jim Kingdon, 24-Aug-2021.)
 |-  ( ph  ->  F : NN --> CC )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( abs `  ( ( F `  k )  -  ( F `  n ) ) )  <  ( C  /  n ) )   &    |-  G  =  ( x  e.  NN  |->  ( Re `  ( F `  x ) ) )   &    |-  H  =  ( x  e.  NN  |->  ( Im `  ( F `
  x ) ) )   &    |-  J  =  ( x  e.  NN  |->  ( _i  x.  ( H `
  x ) ) )   =>    |-  ( ph  ->  F  e.  dom  ~~>  )
 
Theoremclimcvg1n 10100* A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within  C  /  n of the nth term, where  C is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
 |-  ( ph  ->  F : NN --> CC )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( abs `  ( ( F `  k )  -  ( F `  n ) ) )  <  ( C  /  n ) )   =>    |-  ( ph  ->  F  e.  dom  ~~>  )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10511
  Copyright terms: Public domain < Previous  Next >