HomeTheorem List (p. 138 of 393)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 138 of 393) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-26397) |
Hilbert Space Explorer
(26398-27920) |
Users' Mathboxes
(27921-39291) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | iserle 13701* | Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.) |
                 
 
![/\](wedge.gif "/\"){kind=small}  
  | ||
| Theorem | iserge0 13702* | 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 13703* | 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 13704* | 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 | isershft 13705 | Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Mario Carneiro, 5-Nov-2013.) |
 
  | ||
| Theorem | isercolllem1 13706* | Lemma for isercoll 13709. (Contributed by Mario Carneiro, 6-Apr-2015.) |
   
 
 
 | ||
| Theorem | isercolllem2 13707* | Lemma for isercoll 13709. (Contributed by Mario Carneiro, 6-Apr-2015.) |
   | ||
| Theorem | isercolllem3 13708* | Lemma for isercoll 13709. (Contributed by Mario Carneiro, 6-Apr-2015.) |
 ![\](setminus.gif "\"){kind=small} 
| ||
| Theorem | isercoll 13709* | Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015.) |
|
| ||
| Theorem | isercoll2 13710* | Generalize isercoll 13709 so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015.) |
| ||
| Theorem | climsup 13711* | A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.) |
    | ||
| Theorem | climcau 13712* | A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.) |
  
 | ||
| Theorem | climbdd 13713* | A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017.) |
|
| ||
| Theorem | caucvgrlem 13714* | Lemma for caurcvgr 13716. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by AV, 12-Sep-2020.) |
  
  | ||
| Theorem | caucvgrlemOLD 13715* | Lemma for caurcvgr 13716. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.) Obsolete version of caucvgrlem 13714 as of 12-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
|
| ||
| Theorem | caurcvgr 13716* |
A Cauchy sequence of real numbers converges to its limit supremum. The
third hypothesis specifies that is a Cauchy sequence.
(Contributed by Mario Carneiro, 7-May-2016.) (Revised by AV,
12-Sep-2020.)
|
 | ||
| Theorem | caurcvgrOLD 13717* |
A Cauchy sequence of real numbers converges to its limit supremum. The
third hypothesis specifies that is a Cauchy sequence.
(Contributed by Mario Carneiro, 7-May-2016.) Obsolete version of
caurcvgr 13716 as of 12-Sep-2020. (New usage is
discouraged.)
(Proof modification is discouraged.)
|
|
| ||
| Theorem | caucvgrlem2 13718* | Lemma for caucvgr 13719. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Mario Carneiro, 8-May-2016.) |
 | ||
| Theorem | caucvgr 13719* | A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 8-May-2016.) |
|
| ||
| Theorem | caurcvg 13720* |
A Cauchy sequence of real numbers converges to its limit supremum. The
fourth hypothesis specifies that is a Cauchy sequence.
(Contributed by NM, 4-Apr-2005.) (Revised by AV, 12-Sep-2020.)
|
| ||
| Theorem | caurcvgOLD 13721* |
A Cauchy sequence of real numbers converges to its limit supremum. The
fourth hypothesis specifies that is a Cauchy sequence.
(Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro,
8-May-2016.) Obsolete version of caurcvg 13720 as of 12-Sep-2020.
(New usage is discouraged.) (Proof modification is discouraged.)
|
|
| ||
| Theorem | caurcvg2 13722* | A Cauchy sequence of real numbers converges, existence version. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 7-Sep-2014.) |
| ||
| Theorem | caucvg 13723* | A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Proof shortened by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.) |
|
| ||
| Theorem | caucvgb 13724* | A function is convergent if and only if it is Cauchy. Theorem 12-5.3 of [Gleason] p. 180. (Contributed by Mario Carneiro, 15-Feb-2014.) |
|
| ||
| Theorem | serf0 13725* | If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 16-Feb-2014.) |
|
| ||
| Theorem | iseraltlem1 13726* | Lemma for iseralt 13729. A decreasing sequence with limit zero consists of positive terms. (Contributed by Mario Carneiro, 6-Apr-2015.) |
|
| ||
| Theorem | iseraltlem2 13727* |
Lemma for iseralt 13729. The terms of an alternating series form a
chain
of inequalities in alternate terms, so that for example
 and
  (assuming
so that
these terms are defined). (Contributed by Mario Carneiro,
6-Apr-2015.)
|
  
| ||
| Theorem | iseraltlem3 13728* |
Lemma for iseralt 13729. From iseraltlem2 13727, we have
and
,
and we also have
for each by the
definition of the partial sum , so combining the inequalities we
get
, so
and
. Thus, both even and
odd partial sums are Cauchy if converges to . (Contributed
by Mario Carneiro, 6-Apr-2015.)
|
|
| ||
| Theorem | iseralt 13729* |
The alternating series test. If is a decreasing sequence
that converges to , then 
is a convergent series. (Note that the first term is positive if
is even, and negative if is odd. If the parity of your series
does not match up with this, you will need to post-compose the series
with multiplication by using isermulc2 13699.) (Contributed by
Mario Carneiro, 7-Apr-2015.)
|
|
| ||
| Syntax | csu 13730 | 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-sum 13731* |
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. These two methods of summation
produce the same result on their common region of definition (i.e.
finite subsets of the upper integers) by summo 13761. Examples:
  means
 , and
 means 1/2 + 1/4 + 1/8 + ... =
1 (geoihalfsum 13916). (Contributed by NM, 11-Dec-2005.)
(Revised by
Mario Carneiro, 13-Jun-2019.)
|
   ![]_](_urbrack.gif "]_"){kind=small}
   | ||
| Theorem | sumex 13732 | A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
|
| ||
| Theorem | sumeq1 13733 | Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
| ||
| Theorem | nfsum1 13734 | Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
 | ||
| Theorem | nfsum 13735 |
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 | sumeq2w 13736 |
Equality theorem for sum, when the class expressions and are
equal everywhere. Proved using only Extensionality. (Contributed by
Mario Carneiro, 24-Jun-2014.) (Revised by Mario Carneiro,
13-Jun-2019.)
|
| | ||
| Theorem | sumeq2ii 13737* |
Equality theorem for sum, with the class expressions and
guarded by 
to be always sets. (Contributed by Mario Carneiro,
13-Jun-2019.)
|
|
| ||
| Theorem | sumeq2 13738* | Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
|
| ||
| Theorem | cbvsum 13739* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
|
| ||
| Theorem | cbvsumv 13740* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
| | ||
| Theorem | cbvsumi 13741* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) |
|
| ||
| Theorem | sumeq1i 13742* | Equality inference for sum. (Contributed by NM, 2-Jan-2006.) |
|
| ||
| Theorem | sumeq2i 13743* | Equality inference for sum. (Contributed by NM, 3-Dec-2005.) |
| | ||
| Theorem | sumeq12i 13744* | Equality inference for sum. (Contributed by FL, 10-Dec-2006.) |
| ||
| Theorem | sumeq1d 13745* | Equality deduction for sum. (Contributed by NM, 1-Nov-2005.) |
| | ||
| Theorem | sumeq2d 13746* |
Equality deduction for sum. Note that unlike sumeq2dv 13747, may
occur in . (Contributed by NM, 1-Nov-2005.)
|
| | ||
| Theorem | sumeq2dv 13747* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| | ||
| Theorem | sumeq2sdv 13748* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) |
| | ||
| Theorem | 2sumeq2dv 13749* | Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
|
| ||
| Theorem | sumeq12dv 13750* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
|
| ||
| Theorem | sumeq12rdv 13751* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
|
| ||
| Theorem | sum2id 13752* | The second class argument to a sum can be chosen so that it is always a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
|
| ||
| Theorem | sumfc 13753* | 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 Mario Carneiro, 23-Apr-2014.) |
|
| ||
| Theorem | fz1f1o 13754* | A lemma for working with finite sums. (Contributed by Mario Carneiro, 22-Apr-2014.) |
 | ||
| Theorem | sumrblem 13755* | Lemma for sumrb 13757. (Contributed by Mario Carneiro, 12-Aug-2013.) |
|
| ||
| Theorem | fsumcvg 13756* | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) |
|
| ||
| Theorem | sumrb 13757* | Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 9-Apr-2014.) |
|
| ||
| Theorem | summolem3 13758* | Lemma for summo 13761. (Contributed by Mario Carneiro, 29-Mar-2014.) |
|
| ||
| Theorem | summolem2a 13759* | Lemma for summo 13761. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 20-Apr-2014.) |
|
| ||
| Theorem | summolem2 13760* | Lemma for summo 13761. (Contributed by Mario Carneiro, 3-Apr-2014.) |
| ||
| Theorem | summo 13761* | A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
| ||
| Theorem | zsum 13762* | Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) |
|
| ||
| Theorem | isum 13763* | 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 | fsum 13764* | The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Mario Carneiro, 13-Jun-2019.) |
|
| ||
| Theorem | sum0 13765 | Any sum over the empty set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.) |
|
| ||
| Theorem | sumz 13766* | Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.) |
|
| ||
| Theorem | fsumf1o 13767* | Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014.) |
|
| ||
| Theorem | sumss 13768* | Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
|
| ||
| Theorem | fsumss 13769* | Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
|
| ||
| Theorem | sumss2 13770* | Change the index set of a sum by adding zeroes. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario Carneiro, 20-Apr-2014.) |
|
| ||
| Theorem | fsumcvg2 13771* | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) |
|
| ||
| Theorem | fsumsers 13772* | Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 21-Apr-2014.) |
|
| ||
| Theorem | fsumcvg3 13773* | A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.) |
|
| ||
| Theorem | fsumser 13774* | A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition of follows as fsum1 13786 and fsump1i 13808, which should make our notation clear and from which, along with closure fsumcl 13777, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 21-Apr-2014.) |
|
| ||
| Theorem | fsumcl2lem 13775* | - 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 13776* | - 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 13777* |
Closure of a finite sum of complex numbers . (Contributed
by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
|
|
| ||
| Theorem | fsumrecl 13778* | Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
|
| ||
| Theorem | fsumzcl 13779* | Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
|
| ||
| Theorem | fsumnn0cl 13780* | Closure of a finite sum of nonnegative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
|
| ||
| Theorem | fsumrpcl 13781* | Closure of a finite sum of positive reals. (Contributed by Mario Carneiro, 3-Jun-2014.) |
|
| ||
| Theorem | fsumzcl2 13782* | A finite sum with integer summands is an integer. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
|
| ||
| Theorem | fsumadd 13783* | The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
|
| ||
| Theorem | fsumsplit 13784* | Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.) |
  
| ||
| Theorem | sumsn 13785* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
| | ||
| Theorem | fsum1 13786* |
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 13787* | A sum over a pair is the sum of the elements. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
| ||
| Theorem | sumtp 13788* | A sum over a triple is the sum of the elements. (Contributed by AV, 24-Jul-2020.) |
| ||
| Theorem | sumsns 13789* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
|
| ||
| Theorem | fsumm1 13790* | Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 26-Apr-2014.) |
|
| ||
| Theorem | fzosump1 13791* | Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016.) |
|
..^ ..^
| ||
| Theorem | fsum1p 13792* | Separate out the first term in a finite sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.) |
|
| ||
| Theorem | fsummsnunz 13793* | A finite sum with an additional integer summand is an integer. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
 | ||
| Theorem | fsumsplitsnun 13794* | Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
| ||
| Theorem | fsump1 13795* |
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 13796* | An infinite sum equals the value its series converges to. (Contributed by NM, 25-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
|
| ||
| Theorem | isumclim2 13797* | A converging series converges to its infinite sum. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.) |
|
| ||
| Theorem | isumclim3 13798* |
The sequence of partial finite sums of a converging infinite series
converge to the infinite sum of the series. Note that must not
occur in .
(Contributed by NM, 9-Jan-2006.) (Revised by Mario
Carneiro, 23-Apr-2014.)
|
| | ||
| Theorem | sumnul 13799* | The sum of a non-convergent infinite series evaluates to the empty set. (Contributed by Paul Chapman, 4-Nov-2007.) (Revised by Mario Carneiro, 23-Apr-2014.) |
| ||
| Theorem | isumcl 13800* | The sum of a converging infinite series is a complex number. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |