Home | Metamath
Proof Explorer Theorem List (p. 156 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iseraltlem2 15501* | Lemma for iseralt 15503. The terms of an alternating series form a chain of inequalities in alternate terms, so that for example π(1) β€ π(3) β€ π(5) β€ ... and ... β€ π(4) β€ π(2) β€ π(0) (assuming π = 0 so that these terms are defined). (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) & β’ ((π β§ π β π) β (πΉβπ) = ((-1βπ) Β· (πΊβπ))) β β’ ((π β§ π β π β§ πΎ β β0) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· πΎ)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) | ||
Theorem | iseraltlem3 15502* | Lemma for iseralt 15503. From iseraltlem2 15501, we have (-1βπ) Β· π(π + 2π) β€ (-1βπ) Β· π(π) and (-1βπ) Β· π(π + 1) β€ (-1βπ) Β· π(π + 2π + 1), and we also have (-1βπ) Β· π(π + 1) = (-1βπ) Β· π(π) β πΊ(π + 1) for each π by the definition of the partial sum π, so combining the inequalities we get (-1βπ) Β· π(π) β πΊ(π + 1) = (-1βπ) Β· π(π + 1) β€ (-1βπ) Β· π(π + 2π + 1) = (-1βπ) Β· π(π + 2π) β πΊ(π + 2π + 1) β€ (-1βπ) Β· π(π + 2π) β€ (-1βπ) Β· π(π) β€ (-1βπ) Β· π(π) + πΊ(π + 1), so β£ (-1βπ) Β· π(π + 2π + 1) β (-1βπ) Β· π(π) β£ = β£ π(π + 2π + 1) β π(π) β£ β€ πΊ(π + 1) and β£ (-1βπ) Β· π(π + 2π) β (-1βπ) Β· π(π) β£ = β£ π(π + 2π) β π(π) β£ β€ πΊ(π + 1). Thus, both even and odd partial sums are Cauchy if πΊ converges to 0. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) & β’ ((π β§ π β π) β (πΉβπ) = ((-1βπ) Β· (πΊβπ))) β β’ ((π β§ π β π β§ πΎ β β0) β ((absβ((seqπ( + , πΉ)β(π + (2 Β· πΎ))) β (seqπ( + , πΉ)βπ))) β€ (πΊβ(π + 1)) β§ (absβ((seqπ( + , πΉ)β((π + (2 Β· πΎ)) + 1)) β (seqπ( + , πΉ)βπ))) β€ (πΊβ(π + 1)))) | ||
Theorem | iseralt 15503* | The alternating series test. If πΊ(π) is a decreasing sequence that converges to 0, then Ξ£π β π(-1βπ) Β· πΊ(π) 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 -1 using isermulc2 15476.) (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 9-Jul-2022.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) & β’ ((π β§ π β π) β (πΉβπ) = ((-1βπ) Β· (πΊβπ))) β β’ (π β seqπ( + , πΉ) β dom β ) | ||
Syntax | csu 15504 | Extend class notation to include finite and infinite 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.) |
class Ξ£π β π΄ π΅ | ||
Definition | df-sum 15505* | 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. These two methods of summation produce the same result on their common region of definition (i.e., finite sets of integers) by summo 15536. Examples: Ξ£π β {1, 2, 4}π means 1 + 2 + 4 = 7, and Ξ£π β β(1 / (2βπ)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 15701). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ Ξ£π β π΄ π΅ = (β©π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ β¦(πβπ) / πβ¦π΅))βπ)))) | ||
Theorem | sumex 15506 | A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ Ξ£π β π΄ π΅ β V | ||
Theorem | sumeq1 15507 | Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (π΄ = π΅ β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | nfsum1 15508 | Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ β²ππ΄ β β’ β²πΞ£π β π΄ π΅ | ||
Theorem | nfsum 15509* | Bound-variable hypothesis builder for sum: if π₯ is (effectively) not free in π΄ and π΅, it is not free in Ξ£π β π΄π΅. Version of nfsum 15509 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 11-Dec-2005.) (Revised by Gino Giotto, 24-Feb-2024.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯Ξ£π β π΄ π΅ | ||
Theorem | nfsumOLD 15510 | Obsolete version of nfsum 15509 as of 24-Feb-2024. 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.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯Ξ£π β π΄ π΅ | ||
Theorem | sumeq2w 15511 | 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 15512* | Equality theorem for sum, with the class expressions π΅ and πΆ guarded by I to be always sets. (Contributed by Mario Carneiro, 13-Jun-2019.) |
β’ (βπ β π΄ ( I βπ΅) = ( I βπΆ) β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2 15513* | Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
β’ (βπ β π΄ π΅ = πΆ β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | cbvsum 15514* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (π = π β π΅ = πΆ) & β’ β²ππ΄ & β’ β²ππ΄ & β’ β²ππ΅ & β’ β²ππΆ β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | cbvsumv 15515* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
β’ (π = π β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | cbvsumi 15516* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) |
β’ β²ππ΅ & β’ β²ππΆ & β’ (π = π β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | sumeq1i 15517* | Equality inference for sum. (Contributed by NM, 2-Jan-2006.) |
β’ π΄ = π΅ β β’ Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ | ||
Theorem | sumeq2i 15518* | Equality inference for sum. (Contributed by NM, 3-Dec-2005.) |
β’ (π β π΄ β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | sumeq12i 15519* | Equality inference for sum. (Contributed by FL, 10-Dec-2006.) |
β’ π΄ = π΅ & β’ (π β π΄ β πΆ = π·) β β’ Ξ£π β π΄ πΆ = Ξ£π β π΅ π· | ||
Theorem | sumeq1d 15520* | Equality deduction for sum. (Contributed by NM, 1-Nov-2005.) |
β’ (π β π΄ = π΅) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | sumeq2d 15521* | Equality deduction for sum. Note that unlike sumeq2dv 15522, π may occur in π. (Contributed by NM, 1-Nov-2005.) |
β’ (π β βπ β π΄ π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2dv 15522* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ ((π β§ π β π΄) β π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2sdv 15523* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | 2sumeq2dv 15524* | Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ ((π β§ π β π΄ β§ π β π΅) β πΆ = π·) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ πΆ = Ξ£π β π΄ Ξ£π β π΅ π·) | ||
Theorem | sumeq12dv 15525* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
β’ (π β π΄ = π΅) & β’ ((π β§ π β π΄) β πΆ = π·) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ π·) | ||
Theorem | sumeq12rdv 15526* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
β’ (π β π΄ = π΅) & β’ ((π β§ π β π΅) β πΆ = π·) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ π·) | ||
Theorem | sum2id 15527* | 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.) |
β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ ( I βπ΅) | ||
Theorem | sumfc 15528* | 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 15529* | A lemma for working with finite sums. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ (π΄ β Fin β (π΄ = β β¨ ((β―βπ΄) β β β§ βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) | ||
Theorem | sumrblem 15530* | Lemma for sumrb 15532. (Contributed by Mario Carneiro, 12-Aug-2013.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π β (β€β₯βπ)) β β’ ((π β§ π΄ β (β€β₯βπ)) β (seqπ( + , πΉ) βΎ (β€β₯βπ)) = seqπ( + , πΉ)) | ||
Theorem | fsumcvg 15531* | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π β (β€β₯βπ)) & β’ (π β π΄ β (π...π)) β β’ (π β seqπ( + , πΉ) β (seqπ( + , πΉ)βπ)) | ||
Theorem | sumrb 15532* | Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 9-Apr-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π΄ β (β€β₯βπ)) & β’ (π β π΄ β (β€β₯βπ)) β β’ (π β (seqπ( + , πΉ) β πΆ β seqπ( + , πΉ) β πΆ)) | ||
Theorem | summolem3 15533* | Lemma for summo 15536. (Contributed by Mario Carneiro, 29-Mar-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) & β’ π» = (π β β β¦ β¦(πΎβπ) / πβ¦π΅) & β’ (π β (π β β β§ π β β)) & β’ (π β π:(1...π)β1-1-ontoβπ΄) & β’ (π β πΎ:(1...π)β1-1-ontoβπ΄) β β’ (π β (seq1( + , πΊ)βπ) = (seq1( + , π»)βπ)) | ||
Theorem | summolem2a 15534* | Lemma for summo 15536. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 20-Apr-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) & β’ π» = (π β β β¦ β¦(πΎβπ) / πβ¦π΅) & β’ (π β π β β) & β’ (π β π β β€) & β’ (π β π΄ β (β€β₯βπ)) & β’ (π β π:(1...π)β1-1-ontoβπ΄) & β’ (π β πΎ Isom < , < ((1...(β―βπ΄)), π΄)) β β’ (π β seqπ( + , πΉ) β (seq1( + , πΊ)βπ)) | ||
Theorem | summolem2 15535* | Lemma for summo 15536. (Contributed by Mario Carneiro, 3-Apr-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) β β’ ((π β§ βπ β β€ (π΄ β (β€β₯βπ) β§ seqπ( + , πΉ) β π₯)) β (βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π¦ = (seq1( + , πΊ)βπ)) β π₯ = π¦)) | ||
Theorem | summo 15536* | A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) β β’ (π β β*π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ seqπ( + , πΉ) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , πΊ)βπ)))) | ||
Theorem | zsum 15537* | Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β π) & β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = ( β βseqπ( + , πΉ))) | ||
Theorem | isum 15538* | 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.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β Ξ£π β π π΅ = ( β βseqπ( + , πΉ))) | ||
Theorem | fsum 15539* | The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (π = (πΉβπ) β π΅ = πΆ) & β’ (π β π β β) & β’ (π β πΉ:(1...π)β1-1-ontoβπ΄) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β (1...π)) β (πΊβπ) = πΆ) β β’ (π β Ξ£π β π΄ π΅ = (seq1( + , πΊ)βπ)) | ||
Theorem | sum0 15540 | Any sum over the empty set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.) |
β’ Ξ£π β β π΄ = 0 | ||
Theorem | sumz 15541* | Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.) |
β’ ((π΄ β (β€β₯βπ) β¨ π΄ β Fin) β Ξ£π β π΄ 0 = 0) | ||
Theorem | fsumf1o 15542* | Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014.) |
β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β Fin) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) | ||
Theorem | sumss 15543* | Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
β’ (π β π΄ β π΅) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) & β’ (π β π΅ β (β€β₯βπ)) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | fsumss 15544* | Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
β’ (π β π΄ β π΅) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) & β’ (π β π΅ β Fin) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | sumss2 15545* | Change the index set of a sum by adding zeroes. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario Carneiro, 20-Apr-2014.) |
β’ (((π΄ β π΅ β§ βπ β π΄ πΆ β β) β§ (π΅ β (β€β₯βπ) β¨ π΅ β Fin)) β Ξ£π β π΄ πΆ = Ξ£π β π΅ if(π β π΄, πΆ, 0)) | ||
Theorem | fsumcvg2 15546* | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) |
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π΄ β (π...π)) β β’ (π β seqπ( + , πΉ) β (seqπ( + , πΉ)βπ)) | ||
Theorem | fsumsers 15547* | 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.) |
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π΄ β (π...π)) β β’ (π β Ξ£π β π΄ π΅ = (seqπ( + , πΉ)βπ)) | ||
Theorem | fsumcvg3 15548* | A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β Fin) & β’ (π β π΄ β π) & β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β seqπ( + , πΉ) β dom β ) | ||
Theorem | fsumser 15549* | A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 15566 and fsump1i 15588, which should make our notation clear and from which, along with closure fsumcl 15552, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 21-Apr-2014.) |
β’ ((π β§ π β (π...π)) β (πΉβπ) = π΄) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) β β’ (π β Ξ£π β (π...π)π΄ = (seqπ( + , πΉ)βπ)) | ||
Theorem | fsumcl2lem 15550* | - 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.) |
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β π΄ β β ) β β’ (π β Ξ£π β π΄ π΅ β π) | ||
Theorem | fsumcllem 15551* | - 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.) |
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β 0 β π) β β’ (π β Ξ£π β π΄ π΅ β π) | ||
Theorem | fsumcl 15552* | Closure of a finite sum of complex numbers π΄(π). (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumrecl 15553* | Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumzcl 15554* | Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β€) β β’ (π β Ξ£π β π΄ π΅ β β€) | ||
Theorem | fsumnn0cl 15555* | Closure of a finite sum of nonnegative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β0) β β’ (π β Ξ£π β π΄ π΅ β β0) | ||
Theorem | fsumrpcl 15556* | Closure of a finite sum of positive reals. (Contributed by Mario Carneiro, 3-Jun-2014.) |
β’ (π β π΄ β Fin) & β’ (π β π΄ β β ) & β’ ((π β§ π β π΄) β π΅ β β+) β β’ (π β Ξ£π β π΄ π΅ β β+) | ||
Theorem | fsumclf 15557* | Closure of a finite sum of complex numbers π΄(π). A version of fsumcl 15552 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumzcl2 15558* | A finite sum with integer summands is an integer. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β β€) β Ξ£π β π΄ π΅ β β€) | ||
Theorem | fsumadd 15559* | The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) β β’ (π β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ)) | ||
Theorem | fsumsplit 15560* | Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β (π΄ β© π΅) = β ) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β) β β’ (π β Ξ£π β π πΆ = (Ξ£π β π΄ πΆ + Ξ£π β π΅ πΆ)) | ||
Theorem | fsumsplitf 15561* | Split a sum into two parts. A version of fsumsplit 15560 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β (π΄ β© π΅) = β ) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β) β β’ (π β Ξ£π β π πΆ = (Ξ£π β π΄ πΆ + Ξ£π β π΅ πΆ)) | ||
Theorem | sumsnf 15562* | A sum of a singleton is the term. A version of sumsn 15565 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β Ξ£π β {π}π΄ = π΅) | ||
Theorem | fsumsplitsn 15563* | Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ· & β’ (π β π΄ β Fin) & β’ (π β π΅ β π) & β’ (π β Β¬ π΅ β π΄) & β’ ((π β§ π β π΄) β πΆ β β) & β’ (π = π΅ β πΆ = π·) & β’ (π β π· β β) β β’ (π β Ξ£π β (π΄ βͺ {π΅})πΆ = (Ξ£π β π΄ πΆ + π·)) | ||
Theorem | fsumsplit1 15564* | Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ· & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄) & β’ (π = πΆ β π΅ = π·) β β’ (π β Ξ£π β π΄ π΅ = (π· + Ξ£π β (π΄ β {πΆ})π΅)) | ||
Theorem | sumsn 15565* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β Ξ£π β {π}π΄ = π΅) | ||
Theorem | fsum1 15566* | 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 15567* | A sum over a pair is the sum of the elements. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) & β’ (π β (π· β β β§ πΈ β β)) & β’ (π β (π΄ β π β§ π΅ β π)) & β’ (π β π΄ β π΅) β β’ (π β Ξ£π β {π΄, π΅}πΆ = (π· + πΈ)) | ||
Theorem | sumtp 15568* | A sum over a triple is the sum of the elements. (Contributed by AV, 24-Jul-2020.) |
β’ (π = π΄ β π· = πΈ) & β’ (π = π΅ β π· = πΉ) & β’ (π = πΆ β π· = πΊ) & β’ (π β (πΈ β β β§ πΉ β β β§ πΊ β β)) & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β π΄ β π΅) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β πΆ) β β’ (π β Ξ£π β {π΄, π΅, πΆ}π· = ((πΈ + πΉ) + πΊ)) | ||
Theorem | sumsns 15569* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ ((π β π β§ β¦π / πβ¦π΄ β β) β Ξ£π β {π}π΄ = β¦π / πβ¦π΄) | ||
Theorem | fsumm1 15570* | Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 26-Apr-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = (Ξ£π β (π...(π β 1))π΄ + π΅)) | ||
Theorem | fzosump1 15571* | Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β Ξ£π β (π..^(π + 1))π΄ = (Ξ£π β (π..^π)π΄ + π΅)) | ||
Theorem | fsum1p 15572* | Separate out the first term in a finite sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = (π΅ + Ξ£π β ((π + 1)...π)π΄)) | ||
Theorem | fsummsnunz 15573* | A finite sum all of whose summands are integers is itself an integer (case where the summation set is the union of a finite set and a singleton). (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by AV, 17-Dec-2021.) |
β’ ((π΄ β Fin β§ βπ β (π΄ βͺ {π})π΅ β β€) β Ξ£π β (π΄ βͺ {π})π΅ β β€) | ||
Theorem | fsumsplitsnun 15574* | 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.) |
β’ ((π΄ β Fin β§ (π β π β§ π β π΄) β§ βπ β (π΄ βͺ {π})π΅ β β€) β Ξ£π β (π΄ βͺ {π})π΅ = (Ξ£π β π΄ π΅ + β¦π / πβ¦π΅)) | ||
Theorem | fsump1 15575* | The addition of the next term in a finite sum of π΄(π) is the current term plus π΅ i.e. π΄(π + 1). (Contributed by NM, 4-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...(π + 1))) β π΄ β β) & β’ (π = (π + 1) β π΄ = π΅) β β’ (π β Ξ£π β (π...(π + 1))π΄ = (Ξ£π β (π...π)π΄ + π΅)) | ||
Theorem | isumclim 15576* | An infinite sum equals the value its series converges to. (Contributed by NM, 25-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β π΅) β β’ (π β Ξ£π β π π΄ = π΅) | ||
Theorem | isumclim2 15577* | A converging series converges to its infinite sum. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β seqπ( + , πΉ) β Ξ£π β π π΄) | ||
Theorem | isumclim3 15578* | 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.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β dom β ) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β (πΉβπ) = Ξ£π β (π...π)π΄) β β’ (π β πΉ β Ξ£π β π π΄) | ||
Theorem | sumnul 15579* | 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.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β Β¬ seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π π΄ = β ) | ||
Theorem | isumcl 15580* | The sum of a converging infinite series is a complex number. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π π΄ β β) | ||
Theorem | isummulc2 15581* | An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ (π β π΅ β β) β β’ (π β (π΅ Β· Ξ£π β π π΄) = Ξ£π β π (π΅ Β· π΄)) | ||
Theorem | isummulc1 15582* | An infinite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ (π β π΅ β β) β β’ (π β (Ξ£π β π π΄ Β· π΅) = Ξ£π β π (π΄ Β· π΅)) | ||
Theorem | isumdivc 15583* | An infinite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ (π β π΅ β β) & β’ (π β π΅ β 0) β β’ (π β (Ξ£π β π π΄ / π΅) = Ξ£π β π (π΄ / π΅)) | ||
Theorem | isumrecl 15584* | The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π π΄ β β) | ||
Theorem | isumge0 15585* | An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ ((π β§ π β π) β 0 β€ π΄) β β’ (π β 0 β€ Ξ£π β π π΄) | ||
Theorem | isumadd 15586* | Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β (πΊβπ) = π΅) & β’ ((π β§ π β π) β π΅ β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ (π β seqπ( + , πΊ) β dom β ) β β’ (π β Ξ£π β π (π΄ + π΅) = (Ξ£π β π π΄ + Ξ£π β π π΅)) | ||
Theorem | sumsplit 15587* | Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β (π΄ βͺ π΅) β π) & β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, πΆ, 0)) & β’ ((π β§ π β π) β (πΊβπ) = if(π β π΅, πΆ, 0)) & β’ ((π β§ π β (π΄ βͺ π΅)) β πΆ β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ (π β seqπ( + , πΊ) β dom β ) β β’ (π β Ξ£π β (π΄ βͺ π΅)πΆ = (Ξ£π β π΄ πΆ + Ξ£π β π΅ πΆ)) | ||
Theorem | fsump1i 15588* | Optimized version of fsump1 15575 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ π = (πΎ + 1) & β’ (π = π β π΄ = π΅) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β (πΎ β π β§ Ξ£π β (π...πΎ)π΄ = π)) & β’ (π β (π + π΅) = π) β β’ (π β (π β π β§ Ξ£π β (π...π)π΄ = π)) | ||
Theorem | fsum2dlem 15589* | Lemma for fsum2d 15590- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) |
β’ (π§ = β¨π, πβ© β π· = πΆ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β) & β’ (π β Β¬ π¦ β π₯) & β’ (π β (π₯ βͺ {π¦}) β π΄) & β’ (π β Ξ£π β π₯ Ξ£π β π΅ πΆ = Ξ£π§ β βͺ π β π₯ ({π} Γ π΅)π·) β β’ ((π β§ π) β Ξ£π β (π₯ βͺ {π¦})Ξ£π β π΅ πΆ = Ξ£π§ β βͺ π β (π₯ βͺ {π¦})({π} Γ π΅)π·) | ||
Theorem | fsum2d 15590* | 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.) |
β’ (π§ = β¨π, πβ© β π· = πΆ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ πΆ = Ξ£π§ β βͺ π β π΄ ({π} Γ π΅)π·) | ||
Theorem | fsumxp 15591* | Combine two sums into a single sum over the cartesian product. (Contributed by Mario Carneiro, 23-Apr-2014.) |
β’ (π§ = β¨π, πβ© β π· = πΆ) & β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ πΆ = Ξ£π§ β (π΄ Γ π΅)π·) | ||
Theorem | fsumcnv 15592* | Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014.) |
β’ (π₯ = β¨π, πβ© β π΅ = π·) & β’ (π¦ = β¨π, πβ© β πΆ = π·) & β’ (π β π΄ β Fin) & β’ (π β Rel π΄) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β Ξ£π₯ β π΄ π΅ = Ξ£π¦ β β‘ π΄πΆ) | ||
Theorem | fsumcom2 15593* | 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.) |
β’ (π β π΄ β Fin) & β’ (π β πΆ β Fin) & β’ ((π β§ π β π΄) β π΅ β Fin) & β’ (π β ((π β π΄ β§ π β π΅) β (π β πΆ β§ π β π·))) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΈ β β) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ πΈ = Ξ£π β πΆ Ξ£π β π· πΈ) | ||
Theorem | fsumcom 15594* | Interchange order of summation. (Contributed by NM, 15-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ πΆ = Ξ£π β π΅ Ξ£π β π΄ πΆ) | ||
Theorem | fsum0diaglem 15595* | Lemma for fsum0diag 15596. (Contributed by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.) |
β’ ((π β (0...π) β§ π β (0...(π β π))) β (π β (0...π) β§ π β (0...(π β π)))) | ||
Theorem | fsum0diag 15596* | 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.) |
β’ ((π β§ (π β (0...π) β§ π β (0...(π β π)))) β π΄ β β) β β’ (π β Ξ£π β (0...π)Ξ£π β (0...(π β π))π΄ = Ξ£π β (0...π)Ξ£π β (0...(π β π))π΄) | ||
Theorem | mptfzshft 15597* | 1-1 onto function in maps-to notation which shifts a finite set of sequential integers. Formerly part of proof for fsumshft 15599. (Contributed by AV, 24-Aug-2019.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π β ((π + πΎ)...(π + πΎ)) β¦ (π β πΎ)):((π + πΎ)...(π + πΎ))β1-1-ontoβ(π...π)) | ||
Theorem | fsumrev 15598* | Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = (πΎ β π) β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = Ξ£π β ((πΎ β π)...(πΎ β π))π΅) | ||
Theorem | fsumshft 15599* | 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 15600* | Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = (π + πΎ) β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = Ξ£π β ((π β πΎ)...(π β πΎ))π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |