![]() |
Metamath
Proof Explorer Theorem List (p. 150 of 443) | < 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: | ![]() (1-28477) |
![]() (28478-30002) |
![]() (30003-44274) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | serf0 14901* | If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 16-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 0) | ||
Theorem | iseraltlem1 14902* | Lemma for iseralt 14905. A decreasing sequence with limit zero consists of positive terms. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐺:𝑍⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘)) & ⊢ (𝜑 → 𝐺 ⇝ 0) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 0 ≤ (𝐺‘𝑁)) | ||
Theorem | iseraltlem2 14903* | Lemma for iseralt 14905. 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 14904* | Lemma for iseralt 14905. From iseraltlem2 14903, 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 14905* | 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 14878.) (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 9-Jul-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐺:𝑍⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘)) & ⊢ (𝜑 → 𝐺 ⇝ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) | ||
Syntax | csu 14906 | 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 14907* | Define the sum of a series with an index set of integers 𝐴. 𝑘 is normally a free variable in 𝐵, i.e. 𝐵 can be thought of as 𝐵(𝑘). This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. These two methods of summation produce the same result on their common region of definition (i.e. finite sets of integers) by summo 14937. Examples: Σ𝑘 ∈ {1, 2, 4} 𝑘 means 1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 15101). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) | ||
Theorem | sumex 14908 | A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
⊢ Σ𝑘 ∈ 𝐴 𝐵 ∈ V | ||
Theorem | sumeq1 14909 | Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) | ||
Theorem | nfsum1 14910 | Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ Ⅎ𝑘Σ𝑘 ∈ 𝐴 𝐵 | ||
Theorem | nfsum 14911 | Bound-variable hypothesis builder for sum: if 𝑥 is (effectively) not free in 𝐴 and 𝐵, it is not free in Σ𝑘 ∈ 𝐴𝐵. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥Σ𝑘 ∈ 𝐴 𝐵 | ||
Theorem | sumeq2w 14912 | 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 14913* | 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 14914* | Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶) | ||
Theorem | cbvsum 14915* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑘𝐵 & ⊢ Ⅎ𝑗𝐶 ⇒ ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 | ||
Theorem | cbvsumv 14916* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 | ||
Theorem | cbvsumi 14917* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) |
⊢ Ⅎ𝑘𝐵 & ⊢ Ⅎ𝑗𝐶 & ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 | ||
Theorem | sumeq1i 14918* | Equality inference for sum. (Contributed by NM, 2-Jan-2006.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶 | ||
Theorem | sumeq2i 14919* | Equality inference for sum. (Contributed by NM, 3-Dec-2005.) |
⊢ (𝑘 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 | ||
Theorem | sumeq12i 14920* | Equality inference for sum. (Contributed by FL, 10-Dec-2006.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑘 ∈ 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷 | ||
Theorem | sumeq1d 14921* | Equality deduction for sum. (Contributed by NM, 1-Nov-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) | ||
Theorem | sumeq2d 14922* | Equality deduction for sum. Note that unlike sumeq2dv 14923, 𝑘 may occur in 𝜑. (Contributed by NM, 1-Nov-2005.) |
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶) | ||
Theorem | sumeq2dv 14923* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶) | ||
Theorem | sumeq2sdv 14924* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶) | ||
Theorem | 2sumeq2dv 14925* | Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐷) | ||
Theorem | sumeq12dv 14926* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷) | ||
Theorem | sumeq12rdv 14927* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷) | ||
Theorem | sum2id 14928* | 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 14929* | 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 14930* | A lemma for working with finite sums. (Contributed by Mario Carneiro, 22-Apr-2014.) |
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) | ||
Theorem | sumrblem 14931* | Lemma for sumrb 14933. (Contributed by Mario Carneiro, 12-Aug-2013.) |
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( + , 𝐹)) | ||
Theorem | fsumcvg 14932* | 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 14933* | 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 14934* | Lemma for summo 14937. (Contributed by Mario Carneiro, 29-Mar-2014.) |
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⦋(𝐾‘𝑛) / 𝑘⦌𝐵) & ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) & ⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) ⇒ ⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) | ||
Theorem | summolem2a 14935* | Lemma for summo 14937. (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 14936* | Lemma for summo 14937. (Contributed by Mario Carneiro, 3-Apr-2014.) |
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) ⇒ ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦)) | ||
Theorem | summo 14937* | 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 14938* | Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( + , 𝐹))) | ||
Theorem | isum 14939* | 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 14940* | 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 14941 | 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 14942* | 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 14943* | Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014.) |
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) | ||
Theorem | sumss 14944* | Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) & ⊢ (𝜑 → 𝐵 ⊆ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) | ||
Theorem | fsumss 14945* | Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) | ||
Theorem | sumss2 14946* | 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 14947* | 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 14948* | 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 14949* | A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) | ||
Theorem | fsumser 14950* | A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 14965 and fsump1i 14987, which should make our notation clear and from which, along with closure fsumcl 14953, 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 14951* | - 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 14952* | - 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 14953* | Closure of a finite sum of complex numbers 𝐴(𝑘). (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ) | ||
Theorem | fsumrecl 14954* | Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ) | ||
Theorem | fsumzcl 14955* | Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℤ) | ||
Theorem | fsumnn0cl 14956* | Closure of a finite sum of nonnegative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℕ0) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ0) | ||
Theorem | fsumrpcl 14957* | Closure of a finite sum of positive reals. (Contributed by Mario Carneiro, 3-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ+) | ||
Theorem | fsumzcl2 14958* | A finite sum with integer summands is an integer. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℤ) | ||
Theorem | fsumadd 14959* | The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)) | ||
Theorem | fsumsplit 14960* | Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.) |
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶)) | ||
Theorem | fsumsplitf 14961* | Split a sum into two parts. A version of fsumsplit 14960 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶)) | ||
Theorem | sumsnf 14962* | A sum of a singleton is the term. A version of sumsn 14964 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝐵 & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵) | ||
Theorem | fsumsplitsn 14963* | Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐷 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∪ {𝐵})𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + 𝐷)) | ||
Theorem | sumsn 14964* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵) | ||
Theorem | fsum1 14965* | 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 14966* | A sum over a pair is the sum of the elements. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸) & ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ)) & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 + 𝐸)) | ||
Theorem | sumtp 14967* | A sum over a triple is the sum of the elements. (Contributed by AV, 24-Jul-2020.) |
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸) & ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹) & ⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺) & ⊢ (𝜑 → (𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ)) & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 + 𝐹) + 𝐺)) | ||
Theorem | sumsns 14968* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
⊢ ((𝑀 ∈ 𝑉 ∧ ⦋𝑀 / 𝑘⦌𝐴 ∈ ℂ) → Σ𝑘 ∈ {𝑀}𝐴 = ⦋𝑀 / 𝑘⦌𝐴) | ||
Theorem | fsumm1 14969* | Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 26-Apr-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + 𝐵)) | ||
Theorem | fzosump1 14970* | Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (𝑀..^𝑁)𝐴 + 𝐵)) | ||
Theorem | fsum1p 14971* | 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 14972* | 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 14973* | 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 14974* | 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 14975* | 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 14976* | 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 14977* | 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 14978* | 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 14979* | 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 14980* | An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐵 · Σ𝑘 ∈ 𝑍 𝐴) = Σ𝑘 ∈ 𝑍 (𝐵 · 𝐴)) | ||
Theorem | isummulc1 14981* | An infinite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝑍 𝐴 · 𝐵) = Σ𝑘 ∈ 𝑍 (𝐴 · 𝐵)) | ||
Theorem | isumdivc 14982* | 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 14983* | The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℝ) | ||
Theorem | isumge0 14984* | An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ 𝑍 𝐴) | ||
Theorem | isumadd 14985* | Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 (𝐴 + 𝐵) = (Σ𝑘 ∈ 𝑍 𝐴 + Σ𝑘 ∈ 𝑍 𝐵)) | ||
Theorem | sumsplit 14986* | 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 14987* | Optimized version of fsump1 14974 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑁 = (𝐾 + 1) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝐾 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝐾)𝐴 = 𝑆)) & ⊢ (𝜑 → (𝑆 + 𝐵) = 𝑇) ⇒ ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝑁)𝐴 = 𝑇)) | ||
Theorem | fsum2dlem 14988* | Lemma for fsum2d 14989- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → ¬ 𝑦 ∈ 𝑥) & ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴) & ⊢ (𝜓 ↔ Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷) | ||
Theorem | fsum2d 14989* | 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 14990* | Combine two sums into a single sum over the cartesian product. (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ (𝐴 × 𝐵)𝐷) | ||
Theorem | fsumcnv 14991* | Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ (𝑥 = 〈𝑗, 𝑘〉 → 𝐵 = 𝐷) & ⊢ (𝑦 = 〈𝑘, 𝑗〉 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → Rel 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑦 ∈ ◡ 𝐴𝐶) | ||
Theorem | fsumcom2 14992* | 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 14993* | Interchange order of summation. (Contributed by NM, 15-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝐵 Σ𝑗 ∈ 𝐴 𝐶) | ||
Theorem | fsum0diaglem 14994* | Lemma for fsum0diag 14995. (Contributed by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.) |
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑘 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 𝑘)))) | ||
Theorem | fsum0diag 14995* | 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 14996* | 1-1 onto function in maps-to notation which shifts a finite set of sequential integers. Formerly part of proof for fsumshft 14998. (Contributed by AV, 24-Aug-2019.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)):((𝑀 + 𝐾)...(𝑁 + 𝐾))–1-1-onto→(𝑀...𝑁)) | ||
Theorem | fsumrev 14997* | Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑗 = (𝐾 − 𝑘) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝐵) | ||
Theorem | fsumshft 14998* | 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 14999* | Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑗 = (𝑘 + 𝐾) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾))𝐵) | ||
Theorem | fsumrev2 15000* | Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 13-Apr-2016.) |
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑗 = ((𝑀 + 𝑁) − 𝑘) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ (𝑀...𝑁)𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |