Theorem List for Intuitionistic Logic Explorer - 11301-11400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sumfct 11301* |
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 11302* |
A lemma for working with finite sums. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
♯
♯ |
|
Theorem | nnf1o 11303 |
Lemma for sum and product theorems. (Contributed by Jim Kingdon,
15-Aug-2022.)
|
|
|
Theorem | sumrbdclem 11304* |
Lemma for sumrbdc 11306. (Contributed by Mario Carneiro,
12-Aug-2013.)
(Revised by Jim Kingdon, 8-Apr-2023.)
|
DECID
|
|
Theorem | fsum3cvg 11305* |
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 11306* |
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 11307* |
Lemma for summodc 11310. (Contributed by Mario Carneiro,
29-Mar-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
|
|
Theorem | summodclem2a 11308* |
Lemma for summodc 11310. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
DECID ♯
♯
|
|
Theorem | summodclem2 11309* |
Lemma for summodc 11310. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 4-May-2023.)
|
♯
DECID
|
|
Theorem | summodc 11310* |
A sum has at most one limit. (Contributed by Mario Carneiro,
3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)
|
♯
♯
DECID
|
|
Theorem | zsumdc 11311* |
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 11312* |
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 11313* |
Closure for a function used to describe a sum over a nonempty finite
set. (Contributed by Jim Kingdon, 10-Oct-2022.)
|
|
|
Theorem | fsum3 11314* |
The value of a sum over a nonempty finite set. (Contributed by Jim
Kingdon, 10-Oct-2022.)
|
|
|
Theorem | sum0 11315 |
Any sum over the empty set is zero. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|
|
|
Theorem | isumz 11316* |
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 11317* |
Re-index a finite sum using a bijection. (Contributed by Mario
Carneiro, 20-Apr-2014.)
|
|
|
Theorem | isumss 11318* |
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 11319* |
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 11320* |
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 11321* |
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 11322* |
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 11323* |
A finite sum is convergent. (Contributed by Mario Carneiro,
24-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|
DECID
|
|
Theorem | fsum3ser 11324* |
A finite sum expressed in terms of a partial sum of an infinite series.
The recursive definition follows as fsum1 11339 and fsump1 11347, which should
make our notation clear and from which, along with closure fsumcl 11327, we
will derive the basic properties of finite sums. (Contributed by NM,
11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.)
|
|
|
Theorem | fsumcl2lem 11325* |
- 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 11326* |
- 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 11327* |
Closure of a finite sum of complex numbers . (Contributed
by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
|
|
|
Theorem | fsumrecl 11328* |
Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.)
(Revised by Mario Carneiro, 22-Apr-2014.)
|
|
|
Theorem | fsumzcl 11329* |
Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.)
(Revised by Mario Carneiro, 22-Apr-2014.)
|
|
|
Theorem | fsumnn0cl 11330* |
Closure of a finite sum of nonnegative integers. (Contributed by
Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | fsumrpcl 11331* |
Closure of a finite sum of positive reals. (Contributed by Mario
Carneiro, 3-Jun-2014.)
|
|
|
Theorem | fsumzcl2 11332* |
A finite sum with integer summands is an integer. (Contributed by
Alexander van der Vekens, 31-Aug-2018.)
|
|
|
Theorem | fsumadd 11333* |
The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised
by Mario Carneiro, 22-Apr-2014.)
|
|
|
Theorem | fsumsplit 11334* |
Split a sum into two parts. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.)
|
|
|
Theorem | fsumsplitf 11335* |
Split a sum into two parts. A version of fsumsplit 11334 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | sumsnf 11336* |
A sum of a singleton is the term. A version of sumsn 11338 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | fsumsplitsn 11337* |
Separate out a term in a finite sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
|
|
Theorem | sumsn 11338* |
A sum of a singleton is the term. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
|
|
Theorem | fsum1 11339* |
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 11340* |
A sum over a pair is the sum of the elements. (Contributed by Thierry
Arnoux, 12-Dec-2016.)
|
|
|
Theorem | sumtp 11341* |
A sum over a triple is the sum of the elements. (Contributed by AV,
24-Jul-2020.)
|
|
|
Theorem | sumsns 11342* |
A sum of a singleton is the term. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
|
|
Theorem | fsumm1 11343* |
Separate out the last term in a finite sum. (Contributed by Mario
Carneiro, 26-Apr-2014.)
|
|
|
Theorem | fzosump1 11344* |
Separate out the last term in a finite sum. (Contributed by Mario
Carneiro, 13-Apr-2016.)
|
..^ ..^
|
|
Theorem | fsum1p 11345* |
Separate out the first term in a finite sum. (Contributed by NM,
3-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | fsumsplitsnun 11346* |
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 11347* |
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 11348* |
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 11349* |
A converging series converges to its infinite sum. (Contributed by NM,
2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | isumclim3 11350* |
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 11351* |
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 11352* |
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 11353* |
An infinite sum multiplied by a constant. (Contributed by NM,
12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | isummulc1 11354* |
An infinite sum multiplied by a constant. (Contributed by NM,
13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | isumdivapc 11355* |
An infinite sum divided by a constant. (Contributed by NM, 2-Jan-2006.)
(Revised by Mario Carneiro, 23-Apr-2014.)
|
# |
|
Theorem | isumrecl 11356* |
The sum of a converging infinite real series is a real number.
(Contributed by Mario Carneiro, 24-Apr-2014.)
|
|
|
Theorem | isumge0 11357* |
An infinite sum of nonnegative terms is nonnegative. (Contributed by
Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | isumadd 11358* |
Addition of infinite sums. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | sumsplitdc 11359* |
Split a sum into two parts. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
DECID
DECID
|
|
Theorem | fsump1i 11360* |
Optimized version of fsump1 11347 for making sums of a concrete number of
terms. (Contributed by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | fsum2dlemstep 11361* |
Lemma for fsum2d 11362- induction step. (Contributed by Mario
Carneiro,
23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.)
|
|
|
Theorem | fsum2d 11362* |
Write a double sum as a sum over a two-dimensional region. Note that
is a function of . (Contributed by Mario Carneiro,
27-Apr-2014.)
|
|
|
Theorem | fsumxp 11363* |
Combine two sums into a single sum over the cartesian product.
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | fsumcnv 11364* |
Transform a region of summation by using the converse operation.
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | fisumcom2 11365* |
Interchange order of summation. Note that and
are not necessarily constant expressions. (Contributed by Mario
Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.)
(Proof shortened by JJ, 2-Aug-2021.)
|
|
|
Theorem | fsumcom 11366* |
Interchange order of summation. (Contributed by NM, 15-Nov-2005.)
(Revised by Mario Carneiro, 23-Apr-2014.)
|
|
|
Theorem | fsum0diaglem 11367* |
Lemma for fisum0diag 11368. (Contributed by Mario Carneiro,
28-Apr-2014.)
(Revised by Mario Carneiro, 8-Apr-2016.)
|
|
|
Theorem | fisum0diag 11368* |
Two ways to express "the sum of over the
triangular
region , ,
." (Contributed
by NM,
31-Dec-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)
(Revised by Mario Carneiro, 8-Apr-2016.)
|
|
|
Theorem | mptfzshft 11369* |
1-1 onto function in maps-to notation which shifts a finite set of
sequential integers. (Contributed by AV, 24-Aug-2019.)
|
|
|
Theorem | fsumrev 11370* |
Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised
by Mario Carneiro, 24-Apr-2014.)
|
|
|
Theorem | fsumshft 11371* |
Index shift of a finite sum. (Contributed by NM, 27-Nov-2005.)
(Revised by Mario Carneiro, 24-Apr-2014.) (Proof shortened by AV,
8-Sep-2019.)
|
|
|
Theorem | fsumshftm 11372* |
Negative index shift of a finite sum. (Contributed by NM,
28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
|
|
Theorem | fisumrev2 11373* |
Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised
by Mario Carneiro, 13-Apr-2016.)
|
|
|
Theorem | fisum0diag2 11374* |
Two ways to express "the sum of over the
triangular
region ,
,
." (Contributed by
Mario Carneiro, 21-Jul-2014.)
|
|
|
Theorem | fsummulc2 11375* |
A finite sum multiplied by a constant. (Contributed by NM,
12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
|
|
Theorem | fsummulc1 11376* |
A finite sum multiplied by a constant. (Contributed by NM,
13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
|
|
Theorem | fsumdivapc 11377* |
A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006.)
(Revised by Mario Carneiro, 24-Apr-2014.)
|
# |
|
Theorem | fsumneg 11378* |
Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013.)
(Revised by Mario Carneiro, 24-Apr-2014.)
|
|
|
Theorem | fsumsub 11379* |
Split a finite sum over a subtraction. (Contributed by Scott Fenton,
12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
|
|
Theorem | fsum2mul 11380* |
Separate the nested sum of the product .
(Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro,
24-Apr-2014.)
|
|
|
Theorem | fsumconst 11381* |
The sum of constant terms ( is not free in ). (Contributed
by NM, 24-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
♯ |
|
Theorem | fsumdifsnconst 11382* |
The sum of constant terms ( is not free in ) over an index
set excluding a singleton. (Contributed by AV, 7-Jan-2022.)
|
♯ |
|
Theorem | modfsummodlem1 11383* |
Lemma for modfsummod 11385. (Contributed by Alexander van der Vekens,
1-Sep-2018.)
|
|
|
Theorem | modfsummodlemstep 11384* |
Induction step for modfsummod 11385. (Contributed by Alexander van der
Vekens, 1-Sep-2018.) (Revised by Jim Kingdon, 12-Oct-2022.)
|
|
|
Theorem | modfsummod 11385* |
A finite sum modulo a positive integer equals the finite sum of their
summands modulo the positive integer, modulo the positive integer.
(Contributed by Alexander van der Vekens, 1-Sep-2018.)
|
|
|
Theorem | fsumge0 11386* |
If all of the terms of a finite sum are nonnegative, so is the sum.
(Contributed by NM, 26-Dec-2005.) (Revised by Mario Carneiro,
24-Apr-2014.)
|
|
|
Theorem | fsumlessfi 11387* |
A shorter sum of nonnegative terms is no greater than a longer one.
(Contributed by NM, 26-Dec-2005.) (Revised by Jim Kingdon,
12-Oct-2022.)
|
|
|
Theorem | fsumge1 11388* |
A sum of nonnegative numbers is greater than or equal to any one of
its terms. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof
shortened by Mario Carneiro, 4-Jun-2014.)
|
|
|
Theorem | fsum00 11389* |
A sum of nonnegative numbers is zero iff all terms are zero.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario
Carneiro, 24-Apr-2014.)
|
|
|
Theorem | fsumle 11390* |
If all of the terms of finite sums compare, so do the sums.
(Contributed by NM, 11-Dec-2005.) (Proof shortened by Mario Carneiro,
24-Apr-2014.)
|
|
|
Theorem | fsumlt 11391* |
If every term in one finite sum is less than the corresponding term in
another, then the first sum is less than the second. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Jun-2014.)
|
|
|
Theorem | fsumabs 11392* |
Generalized triangle inequality: the absolute value of a finite sum is
less than or equal to the sum of absolute values. (Contributed by NM,
9-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
|
|
Theorem | telfsumo 11393* |
Sum of a telescoping series, using half-open intervals. (Contributed by
Mario Carneiro, 2-May-2016.)
|
..^
|
|
Theorem | telfsumo2 11394* |
Sum of a telescoping series. (Contributed by Mario Carneiro,
2-May-2016.)
|
..^
|
|
Theorem | telfsum 11395* |
Sum of a telescoping series. (Contributed by Scott Fenton,
24-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|
|
|
Theorem | telfsum2 11396* |
Sum of a telescoping series. (Contributed by Mario Carneiro,
15-Jun-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|
|
|
Theorem | fsumparts 11397* |
Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
|
..^ ..^ |
|
Theorem | fsumrelem 11398* |
Lemma for fsumre 11399, fsumim 11400, and fsumcj 11401. (Contributed by Mario
Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.)
|
|
|
Theorem | fsumre 11399* |
The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.)
(Revised by Mario Carneiro, 25-Jul-2014.)
|
|
|
Theorem | fsumim 11400* |
The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.)
(Revised by Mario Carneiro, 25-Jul-2014.)
|
|