Type | Label | Description |
Statement |
|
Theorem | climconst2 11301 |
A constant sequence converges to its value. (Contributed by NM,
6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
          
  |
|
Theorem | climz 11302 |
The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
   
 |
|
Theorem | climuni 11303 |
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 11304 |
The limit relation is function-like, and with codomian the complex
numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
|
   |
|
Theorem | climdm 11305 |
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 11306* |
An infinite sequence of complex numbers converges to at most one limit.
(Contributed by NM, 25-Dec-2005.)
|


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

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

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

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

                                                                       
      |
|
Theorem | addcn2 11320* |
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 14137
for the abbreviated version.) (Contributed by Mario Carneiro,
31-Jan-2014.)
|
 
            
     
              |
|
Theorem | subcn2 11321* |
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 11322* |
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 11323* |
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 11324* |
A sufficient condition for a function to be continuous. (Contributed by
Mario Carneiro, 9-Feb-2014.)
|
                    
                                    |
|
Theorem | abscn2 11325* |
The absolute value function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
           
                 |
|
Theorem | cjcn2 11326* |
The complex conjugate function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
           
       
         |
|
Theorem | recn2 11327* |
The real part function is continuous. (Contributed by Mario Carneiro,
9-Feb-2014.)
|
           
       
         |
|
Theorem | imcn2 11328* |
The imaginary part function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
           
       
         |
|
Theorem | climcn1lem 11329* |
The limit of a continuous function, theorem form. (Contributed by
Mario Carneiro, 9-Feb-2014.)
|
                                 
       
                        
      |
|
Theorem | climabs 11330* |
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 11331* |
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 11332* |
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 11333* |
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 11334* |
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 11335* |
A nonnegative sequence converges to a nonnegative number. (Contributed
by NM, 11-Sep-2005.)
|
      
  
        
     
  |
|
Theorem | climadd 11336* |
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 11337* |
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 11338* |
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 11339* |
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 11340* |
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 11341* |
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 11342* |
Limit of a constant
subtracted from each term of a sequence.
(Contributed by Mario Carneiro, 9-Feb-2014.)
|
      
              
         
   
   |
|
Theorem | climsubc2 11343* |
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 11344* |
Comparison of the limits of two sequences. (Contributed by Paul
Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|
      
 
  
               
             |
|
Theorem | climsqz 11345* |
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 11346* |
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 11347* |
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 11348* |
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 11349* |
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 11350* |
Multiplication of an infinite series by a constant. (Contributed by
Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.)
|
          
           
              
     |
|
Theorem | climlec2 11351* |
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 11352* |
Comparison of the limits of two infinite series. (Contributed by Paul
Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.)
|
         
    
  
               
             |
|
Theorem | iserge0 11353* |
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 11354* |
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 11355* |
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 11356* |
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 11357* |
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 11360). 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 11358* |
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 11359* |
Lemma for climcvg1n 11360. 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 11360* |
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 11361* |
A converging sequence of complex numbers is a Cauchy sequence. This is
like climcau 11357 but adds the part that     is complex.
(Contributed by Jim Kingdon, 24-Aug-2021.)
|
        
                           |
|
Theorem | serf0 11362* |
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 11363 |
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 11364* |
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 11532). (Contributed by NM, 11-Dec-2005.)
(Revised by Jim
Kingdon, 21-May-2023.)
|

               DECID  

 
   ![]_ ]_](_urbrack.gif) 
  
                       
 ![]_ ]_](_urbrack.gif)            |
|
Theorem | sumeq1 11365 |
Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jun-2019.)
|
 
   |
|
Theorem | nfsum1 11366 |
Bound-variable hypothesis builder for sum. (Contributed by NM,
11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|
      |
|
Theorem | nfsum 11367 |
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 11368* |
Decidability of a subset of upper integers. (Contributed by Jim
Kingdon, 1-Jan-2022.)
|
              DECID  
 
DECID
  |
|
Theorem | sumeq2 11369* |
Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jul-2013.)
|
  
   |
|
Theorem | cbvsum 11370 |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jun-2019.)
|
          
  |
|
Theorem | cbvsumv 11371* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jul-2013.)
|
     |
|
Theorem | cbvsumi 11372* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
|
    
    |
|
Theorem | sumeq1i 11373* |
Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
|

  |
|
Theorem | sumeq2i 11374* |
Equality inference for sum. (Contributed by NM, 3-Dec-2005.)
|
     |
|
Theorem | sumeq12i 11375* |
Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
|
  
  |
|
Theorem | sumeq1d 11376* |
Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
|
       |
|
Theorem | sumeq2d 11377* |
Equality deduction for sum. Note that unlike sumeq2dv 11378, may
occur in . (Contributed by NM, 1-Nov-2005.)
|
        |
|
Theorem | sumeq2dv 11378* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised
by Mario Carneiro, 31-Jan-2014.)
|
         |
|
Theorem | sumeq2ad 11379* |
Equality deduction for sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
       |
|
Theorem | sumeq2sdv 11380* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.)
|
       |
|
Theorem | 2sumeq2dv 11381* |
Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
      
    |
|
Theorem | sumeq12dv 11382* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
      
    |
|
Theorem | sumeq12rdv 11383* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
      
    |
|
Theorem | sumfct 11384* |
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 11385* |
A lemma for working with finite sums. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
 
 ♯ 
      ♯         |
|
Theorem | nnf1o 11386 |
Lemma for sum and product theorems. (Contributed by Jim Kingdon,
15-Aug-2022.)
|
 
                         |
|
Theorem | sumrbdclem 11387* |
Lemma for sumrbdc 11389. (Contributed by Mario Carneiro,
12-Aug-2013.)
(Revised by Jim Kingdon, 8-Apr-2023.)
|
    
             DECID              
       
     |
|
Theorem | fsum3cvg 11388* |
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 11389* |
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 11390* |
Lemma for summodc 11393. (Contributed by Mario Carneiro,
29-Mar-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
    
       
                              
 ![]_ ]_](_urbrack.gif)            
 ![]_ ]_](_urbrack.gif)          
 
      |
|
Theorem | summodclem2a 11391* |
Lemma for summodc 11393. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
    
             DECID     ♯         ![]_ ]_](_urbrack.gif)   
   
      ![]_ ]_](_urbrack.gif)                             ♯         
        |
|
Theorem | summodclem2 11392* |
Lemma for summodc 11393. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 4-May-2023.)
|
    
         ♯         ![]_ ]_](_urbrack.gif)      
          DECID  
                      
   |
|
Theorem | summodc 11393* |
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 11394* |
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 11395* |
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 11396* |
Closure for a function used to describe a sum over a nonempty finite
set. (Contributed by Jim Kingdon, 10-Oct-2022.)
|
      
                
    
               
  |
|
Theorem | fsum3 11397* |
The value of a sum over a nonempty finite set. (Contributed by Jim
Kingdon, 10-Oct-2022.)
|
      
                
    
                 
        |
|
Theorem | sum0 11398 |
Any sum over the empty set is zero. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|

 |
|
Theorem | isumz 11399* |
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 11400* |
Re-index a finite sum using a bijection. (Contributed by Mario
Carneiro, 20-Apr-2014.)
|
  
             
  
       |