Theorem List for Intuitionistic Logic Explorer - 11101-11200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | climsubc1 11101* |
Limit of a constant
subtracted from each term of a sequence.
(Contributed by Mario Carneiro, 9-Feb-2014.)
|
|
|
Theorem | climsubc2 11102* |
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 11103* |
Comparison of the limits of two sequences. (Contributed by Paul
Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|
|
|
Theorem | climsqz 11104* |
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 11105* |
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 11106* |
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 11107* |
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 11108* |
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 11109* |
Multiplication of an infinite series by a constant. (Contributed by
Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.)
|
|
|
Theorem | climlec2 11110* |
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 11111* |
Comparison of the limits of two infinite series. (Contributed by Paul
Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.)
|
|
|
Theorem | iserge0 11112* |
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 11113* |
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 11114* |
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 11115* |
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 11116* |
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 11119). 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 11117* |
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 11118* |
Lemma for climcvg1n 11119. 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 11119* |
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 11120* |
A converging sequence of complex numbers is a Cauchy sequence. This is
like climcau 11116 but adds the part that is complex.
(Contributed by Jim Kingdon, 24-Aug-2021.)
|
|
|
Theorem | serf0 11121* |
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 11122 |
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 11123* |
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 11291). (Contributed by NM,
11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.)
|
DECID
|
|
Theorem | sumeq1 11124 |
Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jun-2019.)
|
|
|
Theorem | nfsum1 11125 |
Bound-variable hypothesis builder for sum. (Contributed by NM,
11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|
|
|
Theorem | nfsum 11126 |
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 11127* |
Decidability of a subset of upper integers. (Contributed by Jim
Kingdon, 1-Jan-2022.)
|
DECID
DECID
|
|
Theorem | sumeq2 11128* |
Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jul-2013.)
|
|
|
Theorem | cbvsum 11129 |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jun-2019.)
|
|
|
Theorem | cbvsumv 11130* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jul-2013.)
|
|
|
Theorem | cbvsumi 11131* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
|
|
|
Theorem | sumeq1i 11132* |
Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
|
|
|
Theorem | sumeq2i 11133* |
Equality inference for sum. (Contributed by NM, 3-Dec-2005.)
|
|
|
Theorem | sumeq12i 11134* |
Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
|
|
|
Theorem | sumeq1d 11135* |
Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
|
|
|
Theorem | sumeq2d 11136* |
Equality deduction for sum. Note that unlike sumeq2dv 11137, may
occur in . (Contributed by NM, 1-Nov-2005.)
|
|
|
Theorem | sumeq2dv 11137* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised
by Mario Carneiro, 31-Jan-2014.)
|
|
|
Theorem | sumeq2ad 11138* |
Equality deduction for sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
|
|
Theorem | sumeq2sdv 11139* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.)
|
|
|
Theorem | 2sumeq2dv 11140* |
Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
|
|
Theorem | sumeq12dv 11141* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
|
|
Theorem | sumeq12rdv 11142* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
|
|
Theorem | sumfct 11143* |
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 11144* |
A lemma for working with finite sums. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
♯
♯ |
|
Theorem | nnf1o 11145 |
Lemma for sum and product theorems. (Contributed by Jim Kingdon,
15-Aug-2022.)
|
|
|
Theorem | sumrbdclem 11146* |
Lemma for sumrbdc 11148. (Contributed by Mario Carneiro,
12-Aug-2013.)
(Revised by Jim Kingdon, 8-Apr-2023.)
|
DECID
|
|
Theorem | fsum3cvg 11147* |
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 11148* |
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 11149* |
Lemma for summodc 11152. (Contributed by Mario Carneiro,
29-Mar-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
|
|
Theorem | summodclem2a 11150* |
Lemma for summodc 11152. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
DECID ♯
♯
|
|
Theorem | summodclem2 11151* |
Lemma for summodc 11152. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 4-May-2023.)
|
♯
DECID
|
|
Theorem | summodc 11152* |
A sum has at most one limit. (Contributed by Mario Carneiro,
3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)
|
♯
♯
DECID
|
|
Theorem | zsumdc 11153* |
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 11154* |
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 11155* |
Closure for a function used to describe a sum over a nonempty finite
set. (Contributed by Jim Kingdon, 10-Oct-2022.)
|
|
|
Theorem | fsum3 11156* |
The value of a sum over a nonempty finite set. (Contributed by Jim
Kingdon, 10-Oct-2022.)
|
|
|
Theorem | sum0 11157 |
Any sum over the empty set is zero. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|
|
|
Theorem | isumz 11158* |
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 11159* |
Re-index a finite sum using a bijection. (Contributed by Mario
Carneiro, 20-Apr-2014.)
|
|
|
Theorem | isumss 11160* |
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 11161* |
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 11162* |
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 11163* |
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 11164* |
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 11165* |
A finite sum is convergent. (Contributed by Mario Carneiro,
24-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|
DECID
|
|
Theorem | fsum3ser 11166* |
A finite sum expressed in terms of a partial sum of an infinite series.
The recursive definition follows as fsum1 11181 and fsump1 11189, which should
make our notation clear and from which, along with closure fsumcl 11169, we
will derive the basic properties of finite sums. (Contributed by NM,
11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.)
|
|
|
Theorem | fsumcl2lem 11167* |
- 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 11168* |
- 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 11169* |
Closure of a finite sum of complex numbers . (Contributed
by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
|
|
|
Theorem | fsumrecl 11170* |
Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.)
(Revised by Mario Carneiro, 22-Apr-2014.)
|
|
|
Theorem | fsumzcl 11171* |
Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.)
(Revised by Mario Carneiro, 22-Apr-2014.)
|
|
|
Theorem | fsumnn0cl 11172* |
Closure of a finite sum of nonnegative integers. (Contributed by
Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | fsumrpcl 11173* |
Closure of a finite sum of positive reals. (Contributed by Mario
Carneiro, 3-Jun-2014.)
|
|
|
Theorem | fsumzcl2 11174* |
A finite sum with integer summands is an integer. (Contributed by
Alexander van der Vekens, 31-Aug-2018.)
|
|
|
Theorem | fsumadd 11175* |
The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised
by Mario Carneiro, 22-Apr-2014.)
|
|
|
Theorem | fsumsplit 11176* |
Split a sum into two parts. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.)
|
|
|
Theorem | fsumsplitf 11177* |
Split a sum into two parts. A version of fsumsplit 11176 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | sumsnf 11178* |
A sum of a singleton is the term. A version of sumsn 11180 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | fsumsplitsn 11179* |
Separate out a term in a finite sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
|
|
Theorem | sumsn 11180* |
A sum of a singleton is the term. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
|
|
Theorem | fsum1 11181* |
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 11182* |
A sum over a pair is the sum of the elements. (Contributed by Thierry
Arnoux, 12-Dec-2016.)
|
|
|
Theorem | sumtp 11183* |
A sum over a triple is the sum of the elements. (Contributed by AV,
24-Jul-2020.)
|
|
|
Theorem | sumsns 11184* |
A sum of a singleton is the term. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
|
|
Theorem | fsumm1 11185* |
Separate out the last term in a finite sum. (Contributed by Mario
Carneiro, 26-Apr-2014.)
|
|
|
Theorem | fzosump1 11186* |
Separate out the last term in a finite sum. (Contributed by Mario
Carneiro, 13-Apr-2016.)
|
..^ ..^
|
|
Theorem | fsum1p 11187* |
Separate out the first term in a finite sum. (Contributed by NM,
3-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | fsumsplitsnun 11188* |
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.)
|
|
|
Theorem | fsump1 11189* |
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 11190* |
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 11191* |
A converging series converges to its infinite sum. (Contributed by NM,
2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | isumclim3 11192* |
The sequence of partial finite sums of a converging infinite series
converges 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 11193* |
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 11194* |
The sum of a converging infinite series is a complex number.
(Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2014.)
|
|
|
Theorem | isummulc2 11195* |
An infinite sum multiplied by a constant. (Contributed by NM,
12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | isummulc1 11196* |
An infinite sum multiplied by a constant. (Contributed by NM,
13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | isumdivapc 11197* |
An infinite sum divided by a constant. (Contributed by NM, 2-Jan-2006.)
(Revised by Mario Carneiro, 23-Apr-2014.)
|
# |
|
Theorem | isumrecl 11198* |
The sum of a converging infinite real series is a real number.
(Contributed by Mario Carneiro, 24-Apr-2014.)
|
|
|
Theorem | isumge0 11199* |
An infinite sum of nonnegative terms is nonnegative. (Contributed by
Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | isumadd 11200* |
Addition of infinite sums. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
|