Theorem List for Intuitionistic Logic Explorer - 10901-11000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | climuni 10901 |
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 10902 |
The limit relation is function-like, and with range the complex numbers.
(Contributed by Mario Carneiro, 31-Jan-2014.)
|
   |
|
Theorem | climdm 10903 |
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 10904* |
An infinite sequence of complex numbers converges to at most one limit.
(Contributed by NM, 25-Dec-2005.)
|


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

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

 |
|
Theorem | climeq 10907* |
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 10908* |
Exhibit a function
with the same convergence properties as the
not-quite-function . (Contributed by Mario Carneiro,
31-Jan-2014.)
|
             
   |
|
Theorem | 2clim 10909* |
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 10910 |
A shifted function converges if the original function converges.
(Contributed by Mario Carneiro, 5-Nov-2013.)
|
   
 
   |
|
Theorem | climres 10911 |
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 10912 |
A shifted function converges iff the original function converges.
(Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro,
31-Jan-2014.)
|
     
   |
|
Theorem | serclim0 10913 |
The zero series converges to zero. (Contributed by Paul Chapman,
9-Feb-2008.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
|
           
  |
|
Theorem | climshft2 10914* |
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 10915* |
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 10916* |
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
                     

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

                                                                       
      |
|
Theorem | addcn2 10918* |
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.)
|
 
            
     
              |
|
Theorem | subcn2 10919* |
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 10920* |
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 10921* |
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 2100. (Contributed by Mario Carneiro,
9-Feb-2014.)
Using apart, infimum of pair. (Revised by Jim Kingdon, 26-May-2023.)
|
inf                     #
 
  #
            
        |
|
Theorem | cn1lem 10922* |
A sufficient condition for a function to be continuous. (Contributed by
Mario Carneiro, 9-Feb-2014.)
|
                    
                                    |
|
Theorem | abscn2 10923* |
The absolute value function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
           
                 |
|
Theorem | cjcn2 10924* |
The complex conjugate function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
           
       
         |
|
Theorem | recn2 10925* |
The real part function is continuous. (Contributed by Mario Carneiro,
9-Feb-2014.)
|
           
       
         |
|
Theorem | imcn2 10926* |
The imaginary part function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
           
       
         |
|
Theorem | climcn1lem 10927* |
The limit of a continuous function, theorem form. (Contributed by
Mario Carneiro, 9-Feb-2014.)
|
                                 
       
                        
      |
|
Theorem | climabs 10928* |
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 10929* |
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 10930* |
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 10931* |
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 10932* |
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 10933* |
A nonnegative sequence converges to a nonnegative number. (Contributed
by NM, 11-Sep-2005.)
|
      
  
        
     
  |
|
Theorem | climadd 10934* |
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 10935* |
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 10936* |
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 10937* |
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 10938* |
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 10939* |
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 10940* |
Limit of a constant
subtracted from each term of a sequence.
(Contributed by Mario Carneiro, 9-Feb-2014.)
|
      
              
         
   
   |
|
Theorem | climsubc2 10941* |
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 10942* |
Comparison of the limits of two sequences. (Contributed by Paul
Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|
      
 
  
               
             |
|
Theorem | climsqz 10943* |
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 10944* |
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 10945* |
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 10946* |
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 10947* |
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 10948* |
Multiplication of an infinite series by a constant. (Contributed by
Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.)
|
          
           
              
     |
|
Theorem | climlec2 10949* |
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 10950* |
Comparison of the limits of two infinite series. (Contributed by Paul
Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.)
|
         
    
  
               
             |
|
Theorem | iserge0 10951* |
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 10952* |
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 10953* |
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 10954* |
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 10955* |
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 10958). 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 10956* |
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 10957* |
Lemma for climcvg1n 10958. 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 10958* |
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 10959* |
A converging sequence of complex numbers is a Cauchy sequence. This is
like climcau 10955 but adds the part that     is complex.
(Contributed by Jim Kingdon, 24-Aug-2021.)
|
        
                           |
|
Theorem | serf0 10960* |
If an infinite series converges, its underlying sequence converges to
zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro,
16-Feb-2014.)
|
          

 
         |
|
3.8.2 Finite and infinite sums
|
|
Syntax | csu 10961 |
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 10962* |
Define the sum of a series with an index set of integers .
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 11130). (Contributed by NM,
11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.)
|

               DECID  

 
   ![]_ ]_](_urbrack.gif) 
  
                       
 ![]_ ]_](_urbrack.gif)            |
|
Theorem | sumeq1 10963 |
Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jun-2019.)
|
 
   |
|
Theorem | nfsum1 10964 |
Bound-variable hypothesis builder for sum. (Contributed by NM,
11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|
      |
|
Theorem | nfsum 10965 |
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 10966* |
Decidability of a subset of upper integers. (Contributed by Jim
Kingdon, 1-Jan-2022.)
|
              DECID  
 
DECID
  |
|
Theorem | sumeq2 10967* |
Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jul-2013.)
|
  
   |
|
Theorem | cbvsum 10968 |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jun-2019.)
|
          
  |
|
Theorem | cbvsumv 10969* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jul-2013.)
|
     |
|
Theorem | cbvsumi 10970* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
|
    
    |
|
Theorem | sumeq1i 10971* |
Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
|

  |
|
Theorem | sumeq2i 10972* |
Equality inference for sum. (Contributed by NM, 3-Dec-2005.)
|
     |
|
Theorem | sumeq12i 10973* |
Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
|
  
  |
|
Theorem | sumeq1d 10974* |
Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
|
       |
|
Theorem | sumeq2d 10975* |
Equality deduction for sum. Note that unlike sumeq2dv 10976, may
occur in . (Contributed by NM, 1-Nov-2005.)
|
        |
|
Theorem | sumeq2dv 10976* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised
by Mario Carneiro, 31-Jan-2014.)
|
         |
|
Theorem | sumeq2ad 10977* |
Equality deduction for sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
       |
|
Theorem | sumeq2sdv 10978* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.)
|
       |
|
Theorem | 2sumeq2dv 10979* |
Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
      
    |
|
Theorem | sumeq12dv 10980* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
      
    |
|
Theorem | sumeq12rdv 10981* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
      
    |
|
Theorem | sumfct 10982* |
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 10983* |
A lemma for working with finite sums. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
 
 ♯ 
      ♯         |
|
Theorem | sumrbdclem 10984* |
Lemma for sumrbdc 10986. (Contributed by Mario Carneiro,
12-Aug-2013.)
(Revised by Jim Kingdon, 8-Apr-2023.)
|
    
             DECID              
       
     |
|
Theorem | fsum3cvg 10985* |
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 10986* |
Rebase the starting point of a sum. (Contributed by Mario Carneiro,
14-Jul-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
|
    
                            
DECID
       
DECID
    
  
   |
|
Theorem | isummolemnm 10987* |
Lemma for summodc 10991. (Contributed by Jim Kingdon, 15-Aug-2022.)
|
    
       
                         |
|
Theorem | summodclem3 10988* |
Lemma for summodc 10991. (Contributed by Mario Carneiro,
29-Mar-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
    
       
                              
 ![]_ ]_](_urbrack.gif)            
 ![]_ ]_](_urbrack.gif)          
 
      |
|
Theorem | summodclem2a 10989* |
Lemma for summodc 10991. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
    
             DECID     ♯         ![]_ ]_](_urbrack.gif)   
   
      ![]_ ]_](_urbrack.gif)                             ♯         
        |
|
Theorem | summodclem2 10990* |
Lemma for summodc 10991. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 4-May-2023.)
|
    
         ♯         ![]_ ]_](_urbrack.gif)      
          DECID  
                      
   |
|
Theorem | summodc 10991* |
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 10992* |
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 10993* |
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 10994* |
Closure for a function used to describe a sum over a nonempty finite
set. (Contributed by Jim Kingdon, 10-Oct-2022.)
|
      
                
    
               
  |
|
Theorem | fsum3 10995* |
The value of a sum over a nonempty finite set. (Contributed by Jim
Kingdon, 10-Oct-2022.)
|
      
                
    
                 
        |
|
Theorem | sum0 10996 |
Any sum over the empty set is zero. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|

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