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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iseraltlem1 15501* | Lemma for iseralt 15504. A decreasing sequence with limit zero consists of positive terms. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) β β’ ((π β§ π β π) β 0 β€ (πΊβπ)) | ||
Theorem | iseraltlem2 15502* | Lemma for iseralt 15504. 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 15503* | Lemma for iseralt 15504. From iseraltlem2 15502, 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 15504* | 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 15477.) (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 9-Jul-2022.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) & β’ ((π β§ π β π) β (πΉβπ) = ((-1βπ) Β· (πΊβπ))) β β’ (π β seqπ( + , πΉ) β dom β ) | ||
Syntax | csu 15505 | 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 15506* | 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 15537. Examples: Ξ£π β {1, 2, 4}π means 1 + 2 + 4 = 7, and Ξ£π β β(1 / (2βπ)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 15702). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ Ξ£π β π΄ π΅ = (β©π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ β¦(πβπ) / πβ¦π΅))βπ)))) | ||
Theorem | sumex 15507 | A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ Ξ£π β π΄ π΅ β V | ||
Theorem | sumeq1 15508 | Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (π΄ = π΅ β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | nfsum1 15509 | Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ β²ππ΄ β β’ β²πΞ£π β π΄ π΅ | ||
Theorem | nfsum 15510* | Bound-variable hypothesis builder for sum: if π₯ is (effectively) not free in π΄ and π΅, it is not free in Ξ£π β π΄π΅. Version of nfsum 15510 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 11-Dec-2005.) (Revised by Gino Giotto, 24-Feb-2024.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯Ξ£π β π΄ π΅ | ||
Theorem | nfsumOLD 15511 | Obsolete version of nfsum 15510 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 15512 | 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 15513* | 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 15514* | Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
β’ (βπ β π΄ π΅ = πΆ β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | cbvsum 15515* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (π = π β π΅ = πΆ) & β’ β²ππ΄ & β’ β²ππ΄ & β’ β²ππ΅ & β’ β²ππΆ β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | cbvsumv 15516* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
β’ (π = π β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | cbvsumi 15517* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) |
β’ β²ππ΅ & β’ β²ππΆ & β’ (π = π β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | sumeq1i 15518* | Equality inference for sum. (Contributed by NM, 2-Jan-2006.) |
β’ π΄ = π΅ β β’ Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ | ||
Theorem | sumeq2i 15519* | Equality inference for sum. (Contributed by NM, 3-Dec-2005.) |
β’ (π β π΄ β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | sumeq12i 15520* | Equality inference for sum. (Contributed by FL, 10-Dec-2006.) |
β’ π΄ = π΅ & β’ (π β π΄ β πΆ = π·) β β’ Ξ£π β π΄ πΆ = Ξ£π β π΅ π· | ||
Theorem | sumeq1d 15521* | Equality deduction for sum. (Contributed by NM, 1-Nov-2005.) |
β’ (π β π΄ = π΅) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | sumeq2d 15522* | Equality deduction for sum. Note that unlike sumeq2dv 15523, π may occur in π. (Contributed by NM, 1-Nov-2005.) |
β’ (π β βπ β π΄ π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2dv 15523* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ ((π β§ π β π΄) β π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2sdv 15524* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | 2sumeq2dv 15525* | Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ ((π β§ π β π΄ β§ π β π΅) β πΆ = π·) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ πΆ = Ξ£π β π΄ Ξ£π β π΅ π·) | ||
Theorem | sumeq12dv 15526* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
β’ (π β π΄ = π΅) & β’ ((π β§ π β π΄) β πΆ = π·) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ π·) | ||
Theorem | sumeq12rdv 15527* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
β’ (π β π΄ = π΅) & β’ ((π β§ π β π΅) β πΆ = π·) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ π·) | ||
Theorem | sum2id 15528* | 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 15529* | 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 15530* | A lemma for working with finite sums. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ (π΄ β Fin β (π΄ = β β¨ ((β―βπ΄) β β β§ βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) | ||
Theorem | sumrblem 15531* | Lemma for sumrb 15533. (Contributed by Mario Carneiro, 12-Aug-2013.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π β (β€β₯βπ)) β β’ ((π β§ π΄ β (β€β₯βπ)) β (seqπ( + , πΉ) βΎ (β€β₯βπ)) = seqπ( + , πΉ)) | ||
Theorem | fsumcvg 15532* | 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 15533* | 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 15534* | Lemma for summo 15537. (Contributed by Mario Carneiro, 29-Mar-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) & β’ π» = (π β β β¦ β¦(πΎβπ) / πβ¦π΅) & β’ (π β (π β β β§ π β β)) & β’ (π β π:(1...π)β1-1-ontoβπ΄) & β’ (π β πΎ:(1...π)β1-1-ontoβπ΄) β β’ (π β (seq1( + , πΊ)βπ) = (seq1( + , π»)βπ)) | ||
Theorem | summolem2a 15535* | Lemma for summo 15537. (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 15536* | Lemma for summo 15537. (Contributed by Mario Carneiro, 3-Apr-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) β β’ ((π β§ βπ β β€ (π΄ β (β€β₯βπ) β§ seqπ( + , πΉ) β π₯)) β (βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π¦ = (seq1( + , πΊ)βπ)) β π₯ = π¦)) | ||
Theorem | summo 15537* | 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 15538* | Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β π) & β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = ( β βseqπ( + , πΉ))) | ||
Theorem | isum 15539* | 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 15540* | 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 15541 | 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 15542* | 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 15543* | Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014.) |
β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β Fin) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) | ||
Theorem | sumss 15544* | Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
β’ (π β π΄ β π΅) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) & β’ (π β π΅ β (β€β₯βπ)) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | fsumss 15545* | Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
β’ (π β π΄ β π΅) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) & β’ (π β π΅ β Fin) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | sumss2 15546* | 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 15547* | 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 15548* | 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 15549* | A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β Fin) & β’ (π β π΄ β π) & β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β seqπ( + , πΉ) β dom β ) | ||
Theorem | fsumser 15550* | A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 15567 and fsump1i 15589, which should make our notation clear and from which, along with closure fsumcl 15553, 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 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 Mario Carneiro, 3-Jun-2014.) |
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β π΄ β β ) β β’ (π β Ξ£π β π΄ π΅ β π) | ||
Theorem | fsumcllem 15552* | - 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 15553* | Closure of a finite sum of complex numbers π΄(π). (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumrecl 15554* | Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumzcl 15555* | Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β€) β β’ (π β Ξ£π β π΄ π΅ β β€) | ||
Theorem | fsumnn0cl 15556* | Closure of a finite sum of nonnegative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β0) β β’ (π β Ξ£π β π΄ π΅ β β0) | ||
Theorem | fsumrpcl 15557* | Closure of a finite sum of positive reals. (Contributed by Mario Carneiro, 3-Jun-2014.) |
β’ (π β π΄ β Fin) & β’ (π β π΄ β β ) & β’ ((π β§ π β π΄) β π΅ β β+) β β’ (π β Ξ£π β π΄ π΅ β β+) | ||
Theorem | fsumclf 15558* | Closure of a finite sum of complex numbers π΄(π). A version of fsumcl 15553 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumzcl2 15559* | A finite sum with integer summands is an integer. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β β€) β Ξ£π β π΄ π΅ β β€) | ||
Theorem | fsumadd 15560* | The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) β β’ (π β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ)) | ||
Theorem | fsumsplit 15561* | Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β (π΄ β© π΅) = β ) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β) β β’ (π β Ξ£π β π πΆ = (Ξ£π β π΄ πΆ + Ξ£π β π΅ πΆ)) | ||
Theorem | fsumsplitf 15562* | Split a sum into two parts. A version of fsumsplit 15561 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β (π΄ β© π΅) = β ) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β) β β’ (π β Ξ£π β π πΆ = (Ξ£π β π΄ πΆ + Ξ£π β π΅ πΆ)) | ||
Theorem | sumsnf 15563* | A sum of a singleton is the term. A version of sumsn 15566 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β Ξ£π β {π}π΄ = π΅) | ||
Theorem | fsumsplitsn 15564* | Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ· & β’ (π β π΄ β Fin) & β’ (π β π΅ β π) & β’ (π β Β¬ π΅ β π΄) & β’ ((π β§ π β π΄) β πΆ β β) & β’ (π = π΅ β πΆ = π·) & β’ (π β π· β β) β β’ (π β Ξ£π β (π΄ βͺ {π΅})πΆ = (Ξ£π β π΄ πΆ + π·)) | ||
Theorem | fsumsplit1 15565* | Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ· & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄) & β’ (π = πΆ β π΅ = π·) β β’ (π β Ξ£π β π΄ π΅ = (π· + Ξ£π β (π΄ β {πΆ})π΅)) | ||
Theorem | sumsn 15566* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β Ξ£π β {π}π΄ = π΅) | ||
Theorem | fsum1 15567* | 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 15568* | A sum over a pair is the sum of the elements. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) & β’ (π β (π· β β β§ πΈ β β)) & β’ (π β (π΄ β π β§ π΅ β π)) & β’ (π β π΄ β π΅) β β’ (π β Ξ£π β {π΄, π΅}πΆ = (π· + πΈ)) | ||
Theorem | sumtp 15569* | A sum over a triple is the sum of the elements. (Contributed by AV, 24-Jul-2020.) |
β’ (π = π΄ β π· = πΈ) & β’ (π = π΅ β π· = πΉ) & β’ (π = πΆ β π· = πΊ) & β’ (π β (πΈ β β β§ πΉ β β β§ πΊ β β)) & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β π΄ β π΅) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β πΆ) β β’ (π β Ξ£π β {π΄, π΅, πΆ}π· = ((πΈ + πΉ) + πΊ)) | ||
Theorem | sumsns 15570* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ ((π β π β§ β¦π / πβ¦π΄ β β) β Ξ£π β {π}π΄ = β¦π / πβ¦π΄) | ||
Theorem | fsumm1 15571* | Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 26-Apr-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = (Ξ£π β (π...(π β 1))π΄ + π΅)) | ||
Theorem | fzosump1 15572* | Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β Ξ£π β (π..^(π + 1))π΄ = (Ξ£π β (π..^π)π΄ + π΅)) | ||
Theorem | fsum1p 15573* | 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 15574* | 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 15575* | 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 15576* | 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 15577* | 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 15578* | 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 15579* | 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 15580* | 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 15581* | 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 15582* | An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ (π β π΅ β β) β β’ (π β (π΅ Β· Ξ£π β π π΄) = Ξ£π β π (π΅ Β· π΄)) | ||
Theorem | isummulc1 15583* | An infinite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ (π β π΅ β β) β β’ (π β (Ξ£π β π π΄ Β· π΅) = Ξ£π β π (π΄ Β· π΅)) | ||
Theorem | isumdivc 15584* | 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 15585* | The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π π΄ β β) | ||
Theorem | isumge0 15586* | An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ ((π β§ π β π) β 0 β€ π΄) β β’ (π β 0 β€ Ξ£π β π π΄) | ||
Theorem | isumadd 15587* | Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β (πΊβπ) = π΅) & β’ ((π β§ π β π) β π΅ β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ (π β seqπ( + , πΊ) β dom β ) β β’ (π β Ξ£π β π (π΄ + π΅) = (Ξ£π β π π΄ + Ξ£π β π π΅)) | ||
Theorem | sumsplit 15588* | 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 15589* | Optimized version of fsump1 15576 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ π = (πΎ + 1) & β’ (π = π β π΄ = π΅) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β (πΎ β π β§ Ξ£π β (π...πΎ)π΄ = π)) & β’ (π β (π + π΅) = π) β β’ (π β (π β π β§ Ξ£π β (π...π)π΄ = π)) | ||
Theorem | fsum2dlem 15590* | Lemma for fsum2d 15591- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) |
β’ (π§ = β¨π, πβ© β π· = πΆ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β) & β’ (π β Β¬ π¦ β π₯) & β’ (π β (π₯ βͺ {π¦}) β π΄) & β’ (π β Ξ£π β π₯ Ξ£π β π΅ πΆ = Ξ£π§ β βͺ π β π₯ ({π} Γ π΅)π·) β β’ ((π β§ π) β Ξ£π β (π₯ βͺ {π¦})Ξ£π β π΅ πΆ = Ξ£π§ β βͺ π β (π₯ βͺ {π¦})({π} Γ π΅)π·) | ||
Theorem | fsum2d 15591* | 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 15592* | Combine two sums into a single sum over the cartesian product. (Contributed by Mario Carneiro, 23-Apr-2014.) |
β’ (π§ = β¨π, πβ© β π· = πΆ) & β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ πΆ = Ξ£π§ β (π΄ Γ π΅)π·) | ||
Theorem | fsumcnv 15593* | Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014.) |
β’ (π₯ = β¨π, πβ© β π΅ = π·) & β’ (π¦ = β¨π, πβ© β πΆ = π·) & β’ (π β π΄ β Fin) & β’ (π β Rel π΄) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β Ξ£π₯ β π΄ π΅ = Ξ£π¦ β β‘ π΄πΆ) | ||
Theorem | fsumcom2 15594* | 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 15595* | Interchange order of summation. (Contributed by NM, 15-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ πΆ = Ξ£π β π΅ Ξ£π β π΄ πΆ) | ||
Theorem | fsum0diaglem 15596* | Lemma for fsum0diag 15597. (Contributed by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.) |
β’ ((π β (0...π) β§ π β (0...(π β π))) β (π β (0...π) β§ π β (0...(π β π)))) | ||
Theorem | fsum0diag 15597* | 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 15598* | 1-1 onto function in maps-to notation which shifts a finite set of sequential integers. Formerly part of proof for fsumshft 15600. (Contributed by AV, 24-Aug-2019.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π β ((π + πΎ)...(π + πΎ)) β¦ (π β πΎ)):((π + πΎ)...(π + πΎ))β1-1-ontoβ(π...π)) | ||
Theorem | fsumrev 15599* | Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = (πΎ β π) β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = Ξ£π β ((πΎ β π)...(πΎ β π))π΅) | ||
Theorem | fsumshft 15600* | 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.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = (π β πΎ) β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = Ξ£π β ((π + πΎ)...(π + πΎ))π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |