Theorem List for Intuitionistic Logic Explorer - 11301-11400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | climre 11301* |
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 11302* |
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 11303* |
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 11304* |
A nonnegative sequence converges to a nonnegative number. (Contributed
by NM, 11-Sep-2005.)
|
      
  
        
     
  |
|
Theorem | climadd 11305* |
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 11306* |
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 11307* |
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 11308* |
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 11309* |
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 11310* |
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 11311* |
Limit of a constant
subtracted from each term of a sequence.
(Contributed by Mario Carneiro, 9-Feb-2014.)
|
      
              
         
   
   |
|
Theorem | climsubc2 11312* |
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 11313* |
Comparison of the limits of two sequences. (Contributed by Paul
Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|
      
 
  
               
             |
|
Theorem | climsqz 11314* |
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 11315* |
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 11316* |
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 11317* |
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 11318* |
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 11319* |
Multiplication of an infinite series by a constant. (Contributed by
Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.)
|
          
           
              
     |
|
Theorem | climlec2 11320* |
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 11321* |
Comparison of the limits of two infinite series. (Contributed by Paul
Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.)
|
         
    
  
               
             |
|
Theorem | iserge0 11322* |
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 11323* |
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 11324* |
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 11325* |
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 11326* |
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 11329). 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 11327* |
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 11328* |
Lemma for climcvg1n 11329. 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 11329* |
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 11330* |
A converging sequence of complex numbers is a Cauchy sequence. This is
like climcau 11326 but adds the part that     is complex.
(Contributed by Jim Kingdon, 24-Aug-2021.)
|
        
                           |
|
Theorem | serf0 11331* |
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 11332 |
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 11333* |
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 11501). (Contributed by NM, 11-Dec-2005.)
(Revised by Jim
Kingdon, 21-May-2023.)
|

               DECID  

 
   ![]_ ]_](_urbrack.gif) 
  
                       
 ![]_ ]_](_urbrack.gif)            |
|
Theorem | sumeq1 11334 |
Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jun-2019.)
|
 
   |
|
Theorem | nfsum1 11335 |
Bound-variable hypothesis builder for sum. (Contributed by NM,
11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|
      |
|
Theorem | nfsum 11336 |
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 11337* |
Decidability of a subset of upper integers. (Contributed by Jim
Kingdon, 1-Jan-2022.)
|
              DECID  
 
DECID
  |
|
Theorem | sumeq2 11338* |
Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jul-2013.)
|
  
   |
|
Theorem | cbvsum 11339 |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jun-2019.)
|
          
  |
|
Theorem | cbvsumv 11340* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jul-2013.)
|
     |
|
Theorem | cbvsumi 11341* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
|
    
    |
|
Theorem | sumeq1i 11342* |
Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
|

  |
|
Theorem | sumeq2i 11343* |
Equality inference for sum. (Contributed by NM, 3-Dec-2005.)
|
     |
|
Theorem | sumeq12i 11344* |
Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
|
  
  |
|
Theorem | sumeq1d 11345* |
Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
|
       |
|
Theorem | sumeq2d 11346* |
Equality deduction for sum. Note that unlike sumeq2dv 11347, may
occur in . (Contributed by NM, 1-Nov-2005.)
|
        |
|
Theorem | sumeq2dv 11347* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised
by Mario Carneiro, 31-Jan-2014.)
|
         |
|
Theorem | sumeq2ad 11348* |
Equality deduction for sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
       |
|
Theorem | sumeq2sdv 11349* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.)
|
       |
|
Theorem | 2sumeq2dv 11350* |
Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
      
    |
|
Theorem | sumeq12dv 11351* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
      
    |
|
Theorem | sumeq12rdv 11352* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
      
    |
|
Theorem | sumfct 11353* |
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 11354* |
A lemma for working with finite sums. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
 
 ♯ 
      ♯         |
|
Theorem | nnf1o 11355 |
Lemma for sum and product theorems. (Contributed by Jim Kingdon,
15-Aug-2022.)
|
 
                         |
|
Theorem | sumrbdclem 11356* |
Lemma for sumrbdc 11358. (Contributed by Mario Carneiro,
12-Aug-2013.)
(Revised by Jim Kingdon, 8-Apr-2023.)
|
    
             DECID              
       
     |
|
Theorem | fsum3cvg 11357* |
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 11358* |
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 11359* |
Lemma for summodc 11362. (Contributed by Mario Carneiro,
29-Mar-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
    
       
                              
 ![]_ ]_](_urbrack.gif)            
 ![]_ ]_](_urbrack.gif)          
 
      |
|
Theorem | summodclem2a 11360* |
Lemma for summodc 11362. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
    
             DECID     ♯         ![]_ ]_](_urbrack.gif)   
   
      ![]_ ]_](_urbrack.gif)                             ♯         
        |
|
Theorem | summodclem2 11361* |
Lemma for summodc 11362. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 4-May-2023.)
|
    
         ♯         ![]_ ]_](_urbrack.gif)      
          DECID  
                      
   |
|
Theorem | summodc 11362* |
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 11363* |
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 11364* |
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 11365* |
Closure for a function used to describe a sum over a nonempty finite
set. (Contributed by Jim Kingdon, 10-Oct-2022.)
|
      
                
    
               
  |
|
Theorem | fsum3 11366* |
The value of a sum over a nonempty finite set. (Contributed by Jim
Kingdon, 10-Oct-2022.)
|
      
                
    
                 
        |
|
Theorem | sum0 11367 |
Any sum over the empty set is zero. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|

 |
|
Theorem | isumz 11368* |
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 11369* |
Re-index a finite sum using a bijection. (Contributed by Mario
Carneiro, 20-Apr-2014.)
|
  
             
  
       |
|
Theorem | isumss 11370* |
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 11371* |
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         |
|
Theorem | isumss2 11372* |
Change the index set of a sum by adding zeroes. The nonzero elements
are in the contained set and the added zeroes compose the rest of
the containing set which needs to be summable. (Contributed by
Mario Carneiro, 15-Jul-2013.) (Revised by Jim Kingdon, 24-Sep-2022.)
|
    DECID       
   
     DECID              |
|
Theorem | fsum3cvg2 11373* |
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,
2-Dec-2022.)
|
      
     
               
    
DECID
         
         |
|
Theorem | fsumsersdc 11374* |
Special case of series sum over a finite upper integer index set.
(Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Jim
Kingdon, 5-May-2023.)
|
      
     
               
    
DECID
                 |
|
Theorem | fsum3cvg3 11375* |
A finite sum is convergent. (Contributed by Mario Carneiro,
24-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|
                 DECID            
        

 |
|
Theorem | fsum3ser 11376* |
A finite sum expressed in terms of a partial sum of an infinite series.
The recursive definition follows as fsum1 11391 and fsump1 11399, which should
make our notation clear and from which, along with closure fsumcl 11379, we
will derive the basic properties of finite sums. (Contributed by NM,
11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.)
|
      
                 
       
        |
|
Theorem | fsumcl2lem 11377* |
- Lemma for finite sum closures. (The "-" before "Lemma"
forces the
math content to be displayed in the Statement List - NM 11-Feb-2008.)
(Contributed by Mario Carneiro, 3-Jun-2014.)
|
    
 
      
        |
|
Theorem | fsumcllem 11378* |
- Lemma for finite sum closures. (The "-" before "Lemma"
forces the
math content to be displayed in the Statement List - NM 11-Feb-2008.)
(Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro,
3-Jun-2014.)
|
    
 
      
        |
|
Theorem | fsumcl 11379* |
Closure of a finite sum of complex numbers    . (Contributed
by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
|
       
  |
|
Theorem | fsumrecl 11380* |
Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.)
(Revised by Mario Carneiro, 22-Apr-2014.)
|
       
  |
|
Theorem | fsumzcl 11381* |
Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.)
(Revised by Mario Carneiro, 22-Apr-2014.)
|
       
  |
|
Theorem | fsumnn0cl 11382* |
Closure of a finite sum of nonnegative integers. (Contributed by
Mario Carneiro, 23-Apr-2015.)
|
       
  |
|
Theorem | fsumrpcl 11383* |
Closure of a finite sum of positive reals. (Contributed by Mario
Carneiro, 3-Jun-2014.)
|
         
  |
|
Theorem | fsumzcl2 11384* |
A finite sum with integer summands is an integer. (Contributed by
Alexander van der Vekens, 31-Aug-2018.)
|
  
 
  |
|
Theorem | fsumadd 11385* |
The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised
by Mario Carneiro, 22-Apr-2014.)
|
       
     
      |
|
Theorem | fsumsplit 11386* |
Split a sum into two parts. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.)
|
                 
    |
|
Theorem | fsumsplitf 11387* |
Split a sum into two parts. A version of fsumsplit 11386 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
                   
    |
|
Theorem | sumsnf 11388* |
A sum of a singleton is the term. A version of sumsn 11390 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
  
          |
|
Theorem | fsumsplitsn 11389* |
Separate out a term in a finite sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
              
           
   |
|
Theorem | sumsn 11390* |
A sum of a singleton is the term. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
           |
|
Theorem | fsum1 11391* |
The finite sum of    from to (i.e. a sum with
only one term) is i.e.    . (Contributed by NM,
8-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
|
             |
|
Theorem | sumpr 11392* |
A sum over a pair is the sum of the elements. (Contributed by Thierry
Arnoux, 12-Dec-2016.)
|
  
 
    
         

   |
|
Theorem | sumtp 11393* |
A sum over a triple is the sum of the elements. (Contributed by AV,
24-Jul-2020.)
|
  
 
 
    
                 
   |
|
Theorem | sumsns 11394* |
A sum of a singleton is the term. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
    ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)   |
|
Theorem | fsumm1 11395* |
Separate out the last term in a finite sum. (Contributed by Mario
Carneiro, 26-Apr-2014.)
|
            
 
       
            |
|
Theorem | fzosump1 11396* |
Separate out the last term in a finite sum. (Contributed by Mario
Carneiro, 13-Apr-2016.)
|
            
 
    ..^       ..^ 
   |
|
Theorem | fsum1p 11397* |
Separate out the first term in a finite sum. (Contributed by NM,
3-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
            
 
       

           |
|
Theorem | fsumsplitsnun 11398* |
Separate out a term in a finite sum by splitting the sum into two parts.
(Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by AV,
17-Dec-2021.)
|
                  
  ![]_ ]_](_urbrack.gif)    |
|
Theorem | fsump1 11399* |
The addition of the next term in a finite sum of    is the
current term plus i.e.    . (Contributed by NM,
4-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
|
           
      
      
    
        |
|
Theorem | isumclim 11400* |
An infinite sum equals the value its series converges to.
(Contributed by NM, 25-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2014.)
|
       
             
  
  |