![]() |
Metamath
Proof Explorer Theorem List (p. 152 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fsummsnunz 15101* | 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 15102* | 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 15103* | 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 15104* | 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 15105* | 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 15106* | 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 15107* | 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 15108* | 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 15109* | An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐵 · Σ𝑘 ∈ 𝑍 𝐴) = Σ𝑘 ∈ 𝑍 (𝐵 · 𝐴)) | ||
Theorem | isummulc1 15110* | An infinite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝑍 𝐴 · 𝐵) = Σ𝑘 ∈ 𝑍 (𝐴 · 𝐵)) | ||
Theorem | isumdivc 15111* | 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 15112* | The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℝ) | ||
Theorem | isumge0 15113* | An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ 𝑍 𝐴) | ||
Theorem | isumadd 15114* | Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 (𝐴 + 𝐵) = (Σ𝑘 ∈ 𝑍 𝐴 + Σ𝑘 ∈ 𝑍 𝐵)) | ||
Theorem | sumsplit 15115* | 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 15116* | Optimized version of fsump1 15103 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑁 = (𝐾 + 1) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝐾 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝐾)𝐴 = 𝑆)) & ⊢ (𝜑 → (𝑆 + 𝐵) = 𝑇) ⇒ ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝑁)𝐴 = 𝑇)) | ||
Theorem | fsum2dlem 15117* | Lemma for fsum2d 15118- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → ¬ 𝑦 ∈ 𝑥) & ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴) & ⊢ (𝜓 ↔ Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷) | ||
Theorem | fsum2d 15118* | 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 15119* | Combine two sums into a single sum over the cartesian product. (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ (𝐴 × 𝐵)𝐷) | ||
Theorem | fsumcnv 15120* | Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ (𝑥 = 〈𝑗, 𝑘〉 → 𝐵 = 𝐷) & ⊢ (𝑦 = 〈𝑘, 𝑗〉 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → Rel 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑦 ∈ ◡ 𝐴𝐶) | ||
Theorem | fsumcom2 15121* | 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 15122* | Interchange order of summation. (Contributed by NM, 15-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝐵 Σ𝑗 ∈ 𝐴 𝐶) | ||
Theorem | fsum0diaglem 15123* | Lemma for fsum0diag 15124. (Contributed by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.) |
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑘 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 𝑘)))) | ||
Theorem | fsum0diag 15124* | 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 15125* | 1-1 onto function in maps-to notation which shifts a finite set of sequential integers. Formerly part of proof for fsumshft 15127. (Contributed by AV, 24-Aug-2019.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)):((𝑀 + 𝐾)...(𝑁 + 𝐾))–1-1-onto→(𝑀...𝑁)) | ||
Theorem | fsumrev 15126* | Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑗 = (𝐾 − 𝑘) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝐵) | ||
Theorem | fsumshft 15127* | 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 15128* | Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑗 = (𝑘 + 𝐾) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾))𝐵) | ||
Theorem | fsumrev2 15129* | Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 13-Apr-2016.) |
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑗 = ((𝑀 + 𝑁) − 𝑘) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ (𝑀...𝑁)𝐵) | ||
Theorem | fsum0diag2 15130* | Two ways to express "the sum of 𝐴(𝑗, 𝑘) over the triangular region 0 ≤ 𝑗, 0 ≤ 𝑘, 𝑗 + 𝑘 ≤ 𝑁". (Contributed by Mario Carneiro, 21-Jul-2014.) |
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐴) & ⊢ (𝑥 = (𝑘 − 𝑗) → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗)))) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)Σ𝑘 ∈ (0...(𝑁 − 𝑗))𝐴 = Σ𝑘 ∈ (0...𝑁)Σ𝑗 ∈ (0...𝑘)𝐶) | ||
Theorem | fsummulc2 15131* | A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶 · Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐶 · 𝐵)) | ||
Theorem | fsummulc1 15132* | A finite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 · 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶)) | ||
Theorem | fsumdivc 15133* | A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 / 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 / 𝐶)) | ||
Theorem | fsumneg 15134* | Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -𝐵 = -Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | fsumsub 15135* | Split a finite sum over a subtraction. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 − 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 − Σ𝑘 ∈ 𝐴 𝐶)) | ||
Theorem | fsum2mul 15136* | Separate the nested sum of the product 𝐶(𝑗) · 𝐷(𝑘). (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 (𝐶 · 𝐷) = (Σ𝑗 ∈ 𝐴 𝐶 · Σ𝑘 ∈ 𝐵 𝐷)) | ||
Theorem | fsumconst 15137* | The sum of constant terms (𝑘 is not free in 𝐵). (Contributed by NM, 24-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵)) | ||
Theorem | fsumdifsnconst 15138* | The sum of constant terms (𝑘 is not free in 𝐶) over an index set excluding a singleton. (Contributed by AV, 7-Jan-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ ℂ) → Σ𝑘 ∈ (𝐴 ∖ {𝐵})𝐶 = (((♯‘𝐴) − 1) · 𝐶)) | ||
Theorem | modfsummodslem1 15139* | Lemma 1 for modfsummods 15140. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
⊢ (∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) | ||
Theorem | modfsummods 15140* | Induction step for modfsummod 15141. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ) → ((Σ𝑘 ∈ 𝐴 𝐵 mod 𝑁) = (Σ𝑘 ∈ 𝐴 (𝐵 mod 𝑁) mod 𝑁) → (Σ𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 mod 𝑁) = (Σ𝑘 ∈ (𝐴 ∪ {𝑧})(𝐵 mod 𝑁) mod 𝑁))) | ||
Theorem | modfsummod 15141* | A finite sum modulo a positive integer equals the finite sum of their summands modulo the positive integer, modulo the positive integer. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 mod 𝑁) = (Σ𝑘 ∈ 𝐴 (𝐵 mod 𝑁) mod 𝑁)) | ||
Theorem | fsumge0 15142* | If all of the terms of a finite sum are nonnegative, so is the sum. (Contributed by NM, 26-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | fsumless 15143* | A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by NM, 26-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | fsumge1 15144* | A sum of nonnegative numbers is greater than or equal to any one of its terms. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) & ⊢ (𝑘 = 𝑀 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝑀 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ≤ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | fsum00 15145* | A sum of nonnegative numbers is zero iff all terms are zero. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 = 0 ↔ ∀𝑘 ∈ 𝐴 𝐵 = 0)) | ||
Theorem | fsumle 15146* | If all of the terms of finite sums compare, so do the sums. (Contributed by NM, 11-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐶) | ||
Theorem | fsumlt 15147* | If every term in one finite sum is less than the corresponding term in another, then the first sum is less than the second. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 < Σ𝑘 ∈ 𝐴 𝐶) | ||
Theorem | fsumabs 15148* | Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘Σ𝑘 ∈ 𝐴 𝐵) ≤ Σ𝑘 ∈ 𝐴 (abs‘𝐵)) | ||
Theorem | telfsumo 15149* | Sum of a telescoping series, using half-open intervals. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵) & ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐸) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 − 𝐶) = (𝐷 − 𝐸)) | ||
Theorem | telfsumo2 15150* | Sum of a telescoping series. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵) & ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐸) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 − 𝐵) = (𝐸 − 𝐷)) | ||
Theorem | telfsum 15151* | Sum of a telescoping series. (Contributed by Scott Fenton, 24-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.) |
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵) & ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷) & ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐸) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)(𝐵 − 𝐶) = (𝐷 − 𝐸)) | ||
Theorem | telfsum2 15152* | Sum of a telescoping series. (Contributed by Mario Carneiro, 15-Jun-2014.) (Revised by Mario Carneiro, 2-May-2016.) |
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵) & ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷) & ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐸) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)(𝐶 − 𝐵) = (𝐸 − 𝐷)) | ||
Theorem | fsumparts 15153* | Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ (𝑘 = 𝑗 → (𝐴 = 𝐵 ∧ 𝑉 = 𝑊)) & ⊢ (𝑘 = (𝑗 + 1) → (𝐴 = 𝐶 ∧ 𝑉 = 𝑋)) & ⊢ (𝑘 = 𝑀 → (𝐴 = 𝐷 ∧ 𝑉 = 𝑌)) & ⊢ (𝑘 = 𝑁 → (𝐴 = 𝐸 ∧ 𝑉 = 𝑍)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑉 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊)) = (((𝐸 · 𝑍) − (𝐷 · 𝑌)) − Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋))) | ||
Theorem | fsumrelem 15154* | Lemma for fsumre 15155, fsumim 15156, and fsumcj 15157. (Contributed by Mario Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐹:ℂ⟶ℂ & ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) + (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵)) | ||
Theorem | fsumre 15155* | The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (ℜ‘𝐵)) | ||
Theorem | fsumim 15156* | The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (ℑ‘𝐵)) | ||
Theorem | fsumcj 15157* | The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (∗‘𝐵)) | ||
Theorem | fsumrlim 15158* | Limit of a finite sum of converging sequences. Note that 𝐶(𝑘) is a collection of functions with implicit parameter 𝑘, each of which converges to 𝐷(𝑘) as 𝑛 ⇝ +∞. (Contributed by Mario Carneiro, 22-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝐵 𝐷) | ||
Theorem | fsumo1 15159* | The finite sum of eventually bounded functions (where the index set 𝐵 does not depend on 𝑥) is eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 22-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ∈ 𝑂(1)) | ||
Theorem | o1fsum 15160* | If 𝐴(𝑘) is O(1), then Σ𝑘 ≤ 𝑥, 𝐴(𝑘) is O(𝑥). (Contributed by Mario Carneiro, 23-May-2016.) |
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑘 ∈ ℕ ↦ 𝐴) ∈ 𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1)) | ||
Theorem | seqabs 15161* | Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values. (Contributed by Mario Carneiro, 26-Mar-2014.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (abs‘(seq𝑀( + , 𝐹)‘𝑁)) ≤ (seq𝑀( + , 𝐺)‘𝑁)) | ||
Theorem | iserabs 15162* | Generalized triangle inequality: the absolute value of an infinite sum is less than or equal to the sum of absolute values. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴) & ⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (abs‘𝐴) ≤ 𝐵) | ||
Theorem | cvgcmp 15163* | A comparison test for convergence of a real infinite series. Exercise 3 of [Gleason] p. 182. (Contributed by NM, 1-May-2005.) (Revised by Mario Carneiro, 24-Mar-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → 0 ≤ (𝐺‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐺‘𝑘) ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ ) | ||
Theorem | cvgcmpub 15164* | An upper bound for the limit of a real infinite series. This theorem can also be used to compare two infinite series. (Contributed by Mario Carneiro, 24-Mar-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴) & ⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐴) | ||
Theorem | cvgcmpce 15165* | A comparison test for convergence of a complex infinite series. (Contributed by NM, 25-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (abs‘(𝐺‘𝑘)) ≤ (𝐶 · (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ ) | ||
Theorem | abscvgcvg 15166* | An absolutely convergent series is convergent. (Contributed by Mario Carneiro, 28-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (abs‘(𝐺‘𝑘))) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ ) | ||
Theorem | climfsum 15167* | Limit of a finite sum of converging sequences. Note that 𝐹(𝑘) is a collection of functions with implicit parameter 𝑘, each of which converges to 𝐵(𝑘) as 𝑛 ⇝ +∞. (Contributed by Mario Carneiro, 22-Jul-2014.) (Proof shortened by Mario Carneiro, 22-May-2016.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐹 ⇝ 𝐵) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑛 ∈ 𝑍)) → (𝐹‘𝑛) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑛)) ⇒ ⊢ (𝜑 → 𝐻 ⇝ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | fsumiun 15168* | Sum over a disjoint indexed union. (Contributed by Mario Carneiro, 1-Jul-2015.) (Revised by Mario Carneiro, 10-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶) | ||
Theorem | hashiun 15169* | The cardinality of a disjoint indexed union. (Contributed by Mario Carneiro, 24-Jan-2015.) (Revised by Mario Carneiro, 10-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 𝐵) = Σ𝑥 ∈ 𝐴 (♯‘𝐵)) | ||
Theorem | hash2iun 15170* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Disj 𝑦 ∈ 𝐵 𝐶) ⇒ ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) = Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 (♯‘𝐶)) | ||
Theorem | hash2iun1dif1 15171* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ 𝐵 = (𝐴 ∖ {𝑥}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Disj 𝑦 ∈ 𝐵 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (♯‘𝐶) = 1) ⇒ ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) = ((♯‘𝐴) · ((♯‘𝐴) − 1))) | ||
Theorem | hashrabrex 15172* | The number of elements in a class abstraction with a restricted existential quantification. (Contributed by Alexander van der Vekens, 29-Jul-2018.) |
⊢ (𝜑 → 𝑌 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → {𝑥 ∈ 𝑋 ∣ 𝜓} ∈ Fin) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝑌 {𝑥 ∈ 𝑋 ∣ 𝜓}) ⇒ ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 𝜓}) = Σ𝑦 ∈ 𝑌 (♯‘{𝑥 ∈ 𝑋 ∣ 𝜓})) | ||
Theorem | hashuni 15173* | The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥) ⇒ ⊢ (𝜑 → (♯‘∪ 𝐴) = Σ𝑥 ∈ 𝐴 (♯‘𝑥)) | ||
Theorem | qshash 15174* | The cardinality of a set with an equivalence relation is the sum of the cardinalities of its equivalence classes. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ (𝜑 → ∼ Er 𝐴) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → (♯‘𝐴) = Σ𝑥 ∈ (𝐴 / ∼ )(♯‘𝑥)) | ||
Theorem | ackbijnn 15175* | Translate the Ackermann bijection ackbij1 9649 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (2↑𝑦)) ⇒ ⊢ 𝐹:(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0 | ||
Theorem | binomlem 15176* | Lemma for binom 15177 (binomial theorem). Inductive step. (Contributed by NM, 6-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜓 → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘)))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵)↑(𝑁 + 1)) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))) | ||
Theorem | binom 15177* | The binomial theorem: (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)). Theorem 15-2.8 of [Gleason] p. 296. This part of the proof sets up the induction and does the base case, with the bulk of the work (the induction step) in binomlem 15176. This is Metamath 100 proof #44. (Contributed by NM, 7-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘)))) | ||
Theorem | binom1p 15178* | Special case of the binomial theorem for (1 + 𝐴)↑𝑁. (Contributed by Paul Chapman, 10-May-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((1 + 𝐴)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘))) | ||
Theorem | binom11 15179* | Special case of the binomial theorem for 2↑𝑁. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝑁 ∈ ℕ0 → (2↑𝑁) = Σ𝑘 ∈ (0...𝑁)(𝑁C𝑘)) | ||
Theorem | binom1dif 15180* | A summation for the difference between ((𝐴 + 1)↑𝑁) and (𝐴↑𝑁). (Contributed by Scott Fenton, 9-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((𝐴 + 1)↑𝑁) − (𝐴↑𝑁)) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘))) | ||
Theorem | bcxmaslem1 15181 | Lemma for bcxmas 15182. (Contributed by Paul Chapman, 18-May-2007.) |
⊢ (𝐴 = 𝐵 → ((𝑁 + 𝐴)C𝐴) = ((𝑁 + 𝐵)C𝐵)) | ||
Theorem | bcxmas 15182* | Parallel summation (Christmas Stocking) theorem for Pascal's Triangle. (Contributed by Paul Chapman, 18-May-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (((𝑁 + 1) + 𝑀)C𝑀) = Σ𝑗 ∈ (0...𝑀)((𝑁 + 𝑗)C𝑗)) | ||
Theorem | incexclem 15183* | Lemma for incexc 15184. (Contributed by Mario Carneiro, 7-Aug-2017.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) | ||
Theorem | incexc 15184* | The inclusion/exclusion principle for counting the elements of a finite union of finite sets. This is Metamath 100 proof #96. (Contributed by Mario Carneiro, 7-Aug-2017.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) | ||
Theorem | incexc2 15185* | The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑛 ∈ (1...(♯‘𝐴))((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘∩ 𝑠))) | ||
Theorem | isumshft 15186* | Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝑗 = (𝐾 + 𝑘) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝑊 𝐴 = Σ𝑘 ∈ 𝑍 𝐵) | ||
Theorem | isumsplit 15187* | Split off the first 𝑁 terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) | ||
Theorem | isum1p 15188* | The infinite sum of a converging infinite series equals the first term plus the infinite sum of the rest of it. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = ((𝐹‘𝑀) + Σ𝑘 ∈ (ℤ≥‘(𝑀 + 1))𝐴)) | ||
Theorem | isumnn0nn 15189* | Sum from 0 to infinity in terms of sum from 1 to infinity. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝑘 = 0 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ ℕ0 𝐴 = (𝐵 + Σ𝑘 ∈ ℕ 𝐴)) | ||
Theorem | isumrpcl 15190* | The infinite sum of positive reals is positive. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑊 𝐴 ∈ ℝ+) | ||
Theorem | isumle 15191* | Comparison of two infinite sums. (Contributed by Paul Chapman, 13-Nov-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ≤ Σ𝑘 ∈ 𝑍 𝐵) | ||
Theorem | isumless 15192* | A finite sum of nonnegative numbers is less than or equal to its limit. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐵) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝑍 𝐵) | ||
Theorem | isumsup2 15193* | An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐺 = seq𝑀( + , 𝐹) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ⇒ ⊢ (𝜑 → 𝐺 ⇝ sup(ran 𝐺, ℝ, < )) | ||
Theorem | isumsup 15194* | An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐺 = seq𝑀( + , 𝐹) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = sup(ran 𝐺, ℝ, < )) | ||
Theorem | isumltss 15195* | A partial sum of a series with positive terms is less than the infinite sum. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 < Σ𝑘 ∈ 𝑍 𝐵) | ||
Theorem | climcndslem1 15196* | Lemma for climcnds 15198: bound the original series by the condensed series. (Contributed by Mario Carneiro, 18-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁)) | ||
Theorem | climcndslem2 15197* | Lemma for climcnds 15198: bound the condensed series by the original series. (Contributed by Mario Carneiro, 18-Jul-2014.) (Proof shortened by AV, 10-Jul-2022.) |
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁)))) | ||
Theorem | climcnds 15198* | The Cauchy condensation test. If 𝑎(𝑘) is a decreasing sequence of nonnegative terms, then Σ𝑘 ∈ ℕ𝑎(𝑘) converges iff Σ𝑛 ∈ ℕ02↑𝑛 · 𝑎(2↑𝑛) converges. (Contributed by Mario Carneiro, 18-Jul-2014.) (Proof shortened by AV, 10-Jul-2022.) |
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) ⇒ ⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq0( + , 𝐺) ∈ dom ⇝ )) | ||
Theorem | divrcnv 15199* | The sequence of reciprocals of real numbers, multiplied by the factor 𝐴, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℂ → (𝑛 ∈ ℝ+ ↦ (𝐴 / 𝑛)) ⇝𝑟 0) | ||
Theorem | divcnv 15200* | The sequence of reciprocals of positive integers, multiplied by the factor 𝐴, converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℂ → (𝑛 ∈ ℕ ↦ (𝐴 / 𝑛)) ⇝ 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |