Type | Label | Description |
Statement |
|
Theorem | climuni 11301 |
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.)
|
 
   |
|
Theorem | fclim 11302 |
The limit relation is function-like, and with codomian the complex
numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
|
   |
|
Theorem | climdm 11303 |
Two ways to express that a function has a limit. (The expression
  is sometimes useful as a shorthand for "the unique limit
of the function "). (Contributed by Mario Carneiro,
18-Mar-2014.)
|
     |
|
Theorem | climeu 11304* |
An infinite sequence of complex numbers converges to at most one limit.
(Contributed by NM, 25-Dec-2005.)
|


  |
|
Theorem | climreu 11305* |
An infinite sequence of complex numbers converges to at most one limit.
(Contributed by NM, 25-Dec-2005.)
|

   |
|
Theorem | climmo 11306* |
An infinite sequence of complex numbers converges to at most one limit.
(Contributed by Mario Carneiro, 13-Jul-2013.)
|

 |
|
Theorem | climeq 11307* |
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.)
|
                      
    |
|
Theorem | climmpt 11308* |
Exhibit a function
with the same convergence properties as the
not-quite-function . (Contributed by Mario Carneiro,
31-Jan-2014.)
|
             
   |
|
Theorem | 2clim 11309* |
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.)
|
                                             |
|
Theorem | climshftlemg 11310 |
A shifted function converges if the original function converges.
(Contributed by Mario Carneiro, 5-Nov-2013.)
|
   
 
   |
|
Theorem | climres 11311 |
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.)
|
         
   |
|
Theorem | climshft 11312 |
A shifted function converges iff the original function converges.
(Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro,
31-Jan-2014.)
|
     
   |
|
Theorem | serclim0 11313 |
The zero series converges to zero. (Contributed by Paul Chapman,
9-Feb-2008.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
|
           
  |
|
Theorem | climshft2 11314* |
A shifted function converges iff the original function converges.
(Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario
Carneiro, 6-Feb-2014.)
|
             
             
   |
|
Theorem | climabs0 11315* |
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.)
|
                   
               
   |
|
Theorem | climcn1 11316* |
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
                     

                                                        |
|
Theorem | climcn2 11317* |
Image of a limit under a continuous map, two-arg version. (Contributed
by Mario Carneiro, 31-Jan-2014.)
|
            
 
            

                                                                       
      |
|
Theorem | addcn2 11318* |
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 addcncntop 14055
for the abbreviated version.) (Contributed by Mario Carneiro,
31-Jan-2014.)
|
 
            
     
              |
|
Theorem | subcn2 11319* |
Complex number subtraction is a continuous function. Part of
Proposition 14-4.16 of [Gleason] p. 243.
(Contributed by Mario
Carneiro, 31-Jan-2014.)
|
 
            
     
              |
|
Theorem | mulcn2 11320* |
Complex number multiplication is a continuous function. Part of
Proposition 14-4.16 of [Gleason] p. 243.
(Contributed by Mario
Carneiro, 31-Jan-2014.)
|
 
            
     
              |
|
Theorem | reccn2ap 11321* |
The reciprocal function is continuous. The class is just for
convenience in writing the proof and typically would be passed in as an
instance of eqid 2177. (Contributed by Mario Carneiro,
9-Feb-2014.)
Using apart, infimum of pair. (Revised by Jim Kingdon, 26-May-2023.)
|
inf                     #
 
  #
            
        |
|
Theorem | cn1lem 11322* |
A sufficient condition for a function to be continuous. (Contributed by
Mario Carneiro, 9-Feb-2014.)
|
                    
                                    |
|
Theorem | abscn2 11323* |
The absolute value function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
           
                 |
|
Theorem | cjcn2 11324* |
The complex conjugate function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
           
       
         |
|
Theorem | recn2 11325* |
The real part function is continuous. (Contributed by Mario Carneiro,
9-Feb-2014.)
|
           
       
         |
|
Theorem | imcn2 11326* |
The imaginary part function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
           
       
         |
|
Theorem | climcn1lem 11327* |
The limit of a continuous function, theorem form. (Contributed by
Mario Carneiro, 9-Feb-2014.)
|
                                 
       
                        
      |
|
Theorem | climabs 11328* |
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.)
|
                                         |
|
Theorem | climcj 11329* |
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.)
|
                                  
      |
|
Theorem | climre 11330* |
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.)
|
                                  
      |
|
Theorem | climim 11331* |
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.)
|
                                  
      |
|
Theorem | climrecl 11332* |
The limit of a convergent real sequence is real. Corollary 12-2.5 of
[Gleason] p. 172. (Contributed by NM,
10-Sep-2005.)
|
      
  
         |
|
Theorem | climge0 11333* |
A nonnegative sequence converges to a nonnegative number. (Contributed
by NM, 11-Sep-2005.)
|
      
  
        
     
  |
|
Theorem | climadd 11334* |
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.)
|
      
              
                        
    |
|
Theorem | climmul 11335* |
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.)
|
      
              
                        
    |
|
Theorem | climsub 11336* |
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.)
|
      
              
                        
    |
|
Theorem | climaddc1 11337* |
Limit of a constant
added to each term of a sequence.
(Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro,
3-Feb-2014.)
|
      
              
         
   
   |
|
Theorem | climaddc2 11338* |
Limit of a constant
added to each term of a sequence.
(Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro,
3-Feb-2014.)
|
      
              
             
   |
|
Theorem | climmulc2 11339* |
Limit of a sequence multiplied by a constant . Corollary
12-2.2 of [Gleason] p. 171.
(Contributed by NM, 24-Sep-2005.)
(Revised by Mario Carneiro, 3-Feb-2014.)
|
      
              
             
   |
|
Theorem | climsubc1 11340* |
Limit of a constant
subtracted from each term of a sequence.
(Contributed by Mario Carneiro, 9-Feb-2014.)
|
      
              
         
   
   |
|
Theorem | climsubc2 11341* |
Limit of a constant
minus each term of a sequence.
(Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro,
9-Feb-2014.)
|
      
              
             
   |
|
Theorem | climle 11342* |
Comparison of the limits of two sequences. (Contributed by Paul
Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|
      
 
  
               
             |
|
Theorem | climsqz 11343* |
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.)
|
      
                    
                
 
  |
|
Theorem | climsqz2 11344* |
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.)
|
      
                    
            
        |
|
Theorem | clim2ser 11345* |
The limit of an infinite series with an initial segment removed.
(Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario
Carneiro, 1-Feb-2014.)
|
       
         
      
          |
|
Theorem | clim2ser2 11346* |
The limit of an infinite series with an initial segment added.
(Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario
Carneiro, 1-Feb-2014.)
|
       
           
    
          |
|
Theorem | iserex 11347* |
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.)
|
       
         
  
  |
|
Theorem | isermulc2 11348* |
Multiplication of an infinite series by a constant. (Contributed by
Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.)
|
          
           
              
     |
|
Theorem | climlec2 11349* |
Comparison of a constant to the limit of a sequence. (Contributed by
NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
|
                   
         |
|
Theorem | iserle 11350* |
Comparison of the limits of two infinite series. (Contributed by Paul
Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.)
|
         
    
  
               
             |
|
Theorem | iserge0 11351* |
The limit of an infinite series of nonnegative reals is nonnegative.
(Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario
Carneiro, 3-Feb-2014.)
|
         
  
        
     
  |
|
Theorem | climub 11352* |
The limit of a monotonic sequence is an upper bound. (Contributed by
NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
|
      
  
            
              |
|
Theorem | climserle 11353* |
The partial sums of a converging infinite series with nonnegative
terms are bounded by its limit. (Contributed by NM, 27-Dec-2005.)
(Revised by Mario Carneiro, 9-Feb-2014.)
|
         
  
        
     
        |
|
Theorem | iser3shft 11354* |
Index shift of the limit of an infinite series. (Contributed by Mario
Carneiro, 6-Sep-2013.) (Revised by Jim Kingdon, 17-Oct-2022.)
|
            
       
 
      
          |
|
Theorem | climcau 11355* |
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 11358). Theorem 12-5.3 of [Gleason] p. 180 (necessity part).
(Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
        
            
        |
|
Theorem | climrecvg1n 11356* |
A Cauchy sequence of real numbers converges, existence version. The
rate of convergence is fixed: all terms after the nth term must be
within of the nth term, where is a constant multiplier.
(Contributed by Jim Kingdon, 23-Aug-2021.)
|
                                 
 |
|
Theorem | climcvg1nlem 11357* |
Lemma for climcvg1n 11358. We construct sequences of the real and
imaginary parts of each term of , show those converge, and use
that to show that converges. (Contributed by Jim Kingdon,
24-Aug-2021.)
|
                                
                              |
|
Theorem | climcvg1n 11358* |
A Cauchy sequence of complex numbers converges, existence version.
The rate of convergence is fixed: all terms after the nth term must be
within of the nth term, where is a constant
multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
|
                                 
 |
|
Theorem | climcaucn 11359* |
A converging sequence of complex numbers is a Cauchy sequence. This is
like climcau 11355 but adds the part that     is complex.
(Contributed by Jim Kingdon, 24-Aug-2021.)
|
        
                           |
|
Theorem | serf0 11360* |
If an infinite series converges, its underlying sequence converges to
zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro,
16-Feb-2014.)
|
          

 
         |
|
4.8.2 Finite and infinite sums
|
|
Syntax | csu 11361 |
Extend class notation to include finite summations. (An underscore was
added to the ASCII token in order to facilitate set.mm text searches,
since "sum" is a commonly used word in comments.)
|
  |
|
Definition | df-sumdc 11362* |
Define the sum of a series with an index set of integers . The
variable is
normally a free variable in , i.e., can
be
thought of as    . This definition is the result of a
collection of discussions over the most general definition for a sum
that does not need the index set to have a specified ordering. This
definition is in two parts, one for finite sums and one for subsets of
the upper integers. When summing over a subset of the upper integers,
we extend the index set to the upper integers by adding zero outside the
domain, and then sum the set in order, setting the result to the limit
of the partial sums, if it exists. This means that conditionally
convergent sums can be evaluated meaningfully. For finite sums, we are
explicitly order-independent, by picking any bijection to a 1-based
finite sequence and summing in the induced order. In both cases we have
an
expression so that we only need to be defined where
. In the infinite case, we also require
that the indexing
set be a decidable subset of an upperset of integers (that is,
membership of integers in it is decidable). These two methods of
summation produce the same result on their common region of definition
(i.e., finite sets of integers). Examples:
      means , and
        means 1/2 + 1/4 + 1/8 + ... = 1
(geoihalfsum 11530). (Contributed by NM, 11-Dec-2005.)
(Revised by Jim
Kingdon, 21-May-2023.)
|

               DECID  

 
   ![]_ ]_](_urbrack.gif) 
  
                       
 ![]_ ]_](_urbrack.gif)            |
|
Theorem | sumeq1 11363 |
Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jun-2019.)
|
 
   |
|
Theorem | nfsum1 11364 |
Bound-variable hypothesis builder for sum. (Contributed by NM,
11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|
      |
|
Theorem | nfsum 11365 |
Bound-variable hypothesis builder for sum: if is (effectively) not
free in and
, it is not free in
  .
(Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro,
13-Jun-2019.)
|
        |
|
Theorem | sumdc 11366* |
Decidability of a subset of upper integers. (Contributed by Jim
Kingdon, 1-Jan-2022.)
|
              DECID  
 
DECID
  |
|
Theorem | sumeq2 11367* |
Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jul-2013.)
|
  
   |
|
Theorem | cbvsum 11368 |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jun-2019.)
|
          
  |
|
Theorem | cbvsumv 11369* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jul-2013.)
|
     |
|
Theorem | cbvsumi 11370* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
|
    
    |
|
Theorem | sumeq1i 11371* |
Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
|

  |
|
Theorem | sumeq2i 11372* |
Equality inference for sum. (Contributed by NM, 3-Dec-2005.)
|
     |
|
Theorem | sumeq12i 11373* |
Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
|
  
  |
|
Theorem | sumeq1d 11374* |
Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
|
       |
|
Theorem | sumeq2d 11375* |
Equality deduction for sum. Note that unlike sumeq2dv 11376, may
occur in . (Contributed by NM, 1-Nov-2005.)
|
        |
|
Theorem | sumeq2dv 11376* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised
by Mario Carneiro, 31-Jan-2014.)
|
         |
|
Theorem | sumeq2ad 11377* |
Equality deduction for sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
       |
|
Theorem | sumeq2sdv 11378* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.)
|
       |
|
Theorem | 2sumeq2dv 11379* |
Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
      
    |
|
Theorem | sumeq12dv 11380* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
      
    |
|
Theorem | sumeq12rdv 11381* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
      
    |
|
Theorem | sumfct 11382* |
A lemma to facilitate conversions from the function form to the
class-variable form of a sum. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Jim Kingdon, 18-Sep-2022.)
|
  
     
   |
|
Theorem | fz1f1o 11383* |
A lemma for working with finite sums. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
 
 ♯ 
      ♯         |
|
Theorem | nnf1o 11384 |
Lemma for sum and product theorems. (Contributed by Jim Kingdon,
15-Aug-2022.)
|
 
                         |
|
Theorem | sumrbdclem 11385* |
Lemma for sumrbdc 11387. (Contributed by Mario Carneiro,
12-Aug-2013.)
(Revised by Jim Kingdon, 8-Apr-2023.)
|
    
             DECID              
       
     |
|
Theorem | fsum3cvg 11386* |
The sequence of partial sums of a finite sum converges to the whole
sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim
Kingdon, 12-Nov-2022.)
|
    
             DECID                
         |
|
Theorem | sumrbdc 11387* |
Rebase the starting point of a sum. (Contributed by Mario Carneiro,
14-Jul-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
|
    
                            
DECID
       
DECID
    
  
   |
|
Theorem | summodclem3 11388* |
Lemma for summodc 11391. (Contributed by Mario Carneiro,
29-Mar-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
    
       
                              
 ![]_ ]_](_urbrack.gif)            
 ![]_ ]_](_urbrack.gif)          
 
      |
|
Theorem | summodclem2a 11389* |
Lemma for summodc 11391. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
    
             DECID     ♯         ![]_ ]_](_urbrack.gif)   
   
      ![]_ ]_](_urbrack.gif)                             ♯         
        |
|
Theorem | summodclem2 11390* |
Lemma for summodc 11391. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 4-May-2023.)
|
    
         ♯         ![]_ ]_](_urbrack.gif)      
          DECID  
                      
   |
|
Theorem | summodc 11391* |
A sum has at most one limit. (Contributed by Mario Carneiro,
3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)
|
    
         ♯         ![]_ ]_](_urbrack.gif)   
   ♯       
 ![]_ ]_](_urbrack.gif)         
   
     DECID  
  
                     |
|
Theorem | zsumdc 11392* |
Series sum with index set a subset of the upper integers.
(Contributed by Mario Carneiro, 13-Jun-2019.) (Revised by Jim
Kingdon, 8-Apr-2023.)
|
                       DECID       
 
    |
|
Theorem | isum 11393* |
Series sum with an upper integer index set (i.e. an infinite series).
(Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario
Carneiro, 7-Apr-2014.)
|
       
           
 
    |
|
Theorem | fsumgcl 11394* |
Closure for a function used to describe a sum over a nonempty finite
set. (Contributed by Jim Kingdon, 10-Oct-2022.)
|
      
                
    
               
  |
|
Theorem | fsum3 11395* |
The value of a sum over a nonempty finite set. (Contributed by Jim
Kingdon, 10-Oct-2022.)
|
      
                
    
                 
        |
|
Theorem | sum0 11396 |
Any sum over the empty set is zero. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|

 |
|
Theorem | isumz 11397* |
Any sum of zero over a summable set is zero. (Contributed by Mario
Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
|
            DECID      |
|
Theorem | fsumf1o 11398* |
Re-index a finite sum using a bijection. (Contributed by Mario
Carneiro, 20-Apr-2014.)
|
  
             
  
       |
|
Theorem | isumss 11399* |
Change the index set to a subset in an upper integer sum.
(Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim
Kingdon, 21-Sep-2022.)
|
       
  
       DECID  
             DECID  
    |
|
Theorem | fisumss 11400* |
Change the index set to a subset in a finite sum. (Contributed by Mario
Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.)
|
       
  
   DECID         |