HomeTheorem List (p. 160 of 509)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 160 of 509) | < 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-31407) |
Hilbert Space Explorer
(31408-32930) |
Users' Mathboxes
(32931-50831) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | fsumcj 15901* | The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (∗‘𝐵)) | ||
| Theorem | fsumrlim 15902* | 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 15903* | 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 15904* | If 𝐴(𝑘) is O(1), then Σ𝑘 ≤ 𝑥, 𝐴(𝑘) is O(𝑥). (Contributed by Mario Carneiro, 23-May-2016.) |
| ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑘 ∈ ℕ ↦ 𝐴) ∈ 𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1)) | ||
| Theorem | seqabs 15905* | 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 15906* | 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 15907* | 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 15908* | 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 15909* | 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 15910* | An absolutely convergent series is convergent. (Contributed by Mario Carneiro, 28-Apr-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (abs‘(𝐺‘𝑘))) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ ) | ||
| Theorem | climfsum 15911* | 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 15912* | 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 15913* | 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 15914* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Disj 𝑦 ∈ 𝐵 𝐶) ⇒ ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) = Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 (♯‘𝐶)) | ||
| Theorem | hash2iun1dif1 15915* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ 𝐵 = (𝐴 ∖ {𝑥}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Disj 𝑦 ∈ 𝐵 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (♯‘𝐶) = 1) ⇒ ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) = ((♯‘𝐴) · ((♯‘𝐴) − 1))) | ||
| Theorem | hashrabrex 15916* | 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 15917* | The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥) ⇒ ⊢ (𝜑 → (♯‘∪ 𝐴) = Σ𝑥 ∈ 𝐴 (♯‘𝑥)) | ||
| Theorem | qshash 15918* | 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 | indsum 15919* | Finite sum of a product with the indicator function / Cartesian product with the indicator function. Note: this theorem cannot be efficiently shortened using sumss2 15816, unless there are some additional auxiliary theorems like (if(𝑥 ∈ 𝐴, 1, 0) · 𝐵) = if(𝑥 ∈ 𝐴, 𝐵, 0). (Contributed by Thierry Arnoux, 14-Aug-2017.) (Proof shortened by AV, 11-Apr-2026.) |
| ⊢ (𝜑 → 𝑂 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑂) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝑂 ((((𝟭‘𝑂)‘𝐴)‘𝑥) · 𝐵) = Σ𝑥 ∈ 𝐴 𝐵) | ||
| Theorem | indsumhash 15920* | The finite sum of the indicator function is the number of elements of the corresponding subset. (Contributed by AV, 10-Apr-2026.) |
| ⊢ 1 = ((𝟭‘𝑂)‘𝐴) ⇒ ⊢ ((𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂) → Σ𝑘 ∈ 𝑂 ( 1 ‘𝑘) = (♯‘𝐴)) | ||
| Theorem | ackbijnn 15921* | Translate the Ackermann bijection ackbij1 10243 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (2↑𝑦)) ⇒ ⊢ 𝐹:(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0 | ||
| Theorem | binomlem 15922* | Lemma for binom 15923 (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 15923* | 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 15922. 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 15924* | Special case of the binomial theorem for (1 + 𝐴)↑𝑁. (Contributed by Paul Chapman, 10-May-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((1 + 𝐴)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘))) | ||
| Theorem | binom11 15925* | Special case of the binomial theorem for 2↑𝑁. (Contributed by Mario Carneiro, 13-Mar-2014.) |
| ⊢ (𝑁 ∈ ℕ0 → (2↑𝑁) = Σ𝑘 ∈ (0...𝑁)(𝑁C𝑘)) | ||
| Theorem | binom1dif 15926* | 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 15927 | Lemma for bcxmas 15928. (Contributed by Paul Chapman, 18-May-2007.) |
| ⊢ (𝐴 = 𝐵 → ((𝑁 + 𝐴)C𝐴) = ((𝑁 + 𝐵)C𝐵)) | ||
| Theorem | bcxmas 15928* | 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 15929* | Lemma for incexc 15930. (Contributed by Mario Carneiro, 7-Aug-2017.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) | ||
| Theorem | incexc 15930* | 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 15931* | 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 15932* | Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝑗 = (𝐾 + 𝑘) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝑊 𝐴 = Σ𝑘 ∈ 𝑍 𝐵) | ||
| Theorem | isumsplit 15933* | 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 15934* | 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 15935* | 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 15936* | 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 15937* | 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 15938* | 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 15939* | 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 15940* | 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 15941* | 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 15942* | Lemma for climcnds 15944: 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 15943* | Lemma for climcnds 15944: 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 15944* | 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 15945* | The sequence of reciprocals of real numbers, multiplied by the factor 𝐴, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.) |
| ⊢ (𝐴 ∈ ℂ → (𝑛 ∈ ℝ+ ↦ (𝐴 / 𝑛)) ⇝𝑟 0) | ||
| Theorem | divcnv 15946* | 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) | ||
| Theorem | flo1 15947 | The floor function satisfies ⌊(𝑥) = 𝑥 + 𝑂(1). (Contributed by Mario Carneiro, 21-May-2016.) |
| ⊢ (𝑥 ∈ ℝ ↦ (𝑥 − (⌊‘𝑥))) ∈ 𝑂(1) | ||
| Theorem | divcnvshft 15948* | Limit of a ratio function. (Contributed by Scott Fenton, 16-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐴 / (𝑘 + 𝐵))) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 0) | ||
| Theorem | supcvg 15949* | Extract a sequence 𝑓 in 𝑋 such that the image of the points in the bounded set 𝐴 converges to the supremum 𝑆 of the set. Similar to Equation 4 of [Kreyszig] p. 144. The proof uses countable choice ax-cc 10441. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
| ⊢ 𝑋 ∈ V & ⊢ 𝑆 = sup(𝐴, ℝ, < ) & ⊢ 𝑅 = (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝐴) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹 ∘ 𝑓) ⇝ 𝑆)) | ||
| Theorem | infcvgaux1i 15950* | Auxiliary theorem for applications of supcvg 15949. Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008.) |
| ⊢ 𝑅 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} & ⊢ (𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ) & ⊢ 𝑍 ∈ 𝑋 & ⊢ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 ⇒ ⊢ (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧) | ||
| Theorem | infcvgaux2i 15951* | Auxiliary theorem for applications of supcvg 15949. (Contributed by NM, 4-Mar-2008.) |
| ⊢ 𝑅 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} & ⊢ (𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ) & ⊢ 𝑍 ∈ 𝑋 & ⊢ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 & ⊢ 𝑆 = -sup(𝑅, ℝ, < ) & ⊢ (𝑦 = 𝐶 → 𝐴 = 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑋 → 𝑆 ≤ 𝐵) | ||
| Theorem | harmonic 15952 | The harmonic series 𝐻 diverges. This fact follows from the stronger emcl 27247, which establishes that the harmonic series grows as log𝑛 + γ + o(1), but this uses a more elementary method, attributed to Nicole Oresme (1323-1382). This is Metamath 100 proof #34. (Contributed by Mario Carneiro, 11-Jul-2014.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)) & ⊢ 𝐻 = seq1( + , 𝐹) ⇒ ⊢ ¬ 𝐻 ∈ dom ⇝ | ||
| Theorem | arisum 15953* | Arithmetic series sum of the first 𝑁 positive integers. This is Metamath 100 proof #68. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 22-May-2014.) |
| ⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)𝑘 = (((𝑁↑2) + 𝑁) / 2)) | ||
| Theorem | arisum2 15954* | Arithmetic series sum of the first 𝑁 nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 2-Aug-2021.) |
| ⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) | ||
| Theorem | trireciplem 15955 | Lemma for trirecip 15956. Show that the sum converges. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1)))) ⇒ ⊢ seq1( + , 𝐹) ⇝ 1 | ||
| Theorem | trirecip 15956 | The sum of the reciprocals of the triangle numbers converge to two. This is Metamath 100 proof #42. (Contributed by Scott Fenton, 23-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
| ⊢ Σ𝑘 ∈ ℕ (2 / (𝑘 · (𝑘 + 1))) = 2 | ||
| Theorem | expcnv 15957* | A sequence of powers of a complex number 𝐴 with absolute value less than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐴) < 1) ⇒ ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) | ||
| Theorem | explecnv 15958* | A sequence of terms converges to zero when it is less than powers of a number 𝐴 whose absolute value is less than 1. (Contributed by NM, 19-Jul-2008.) (Revised by Mario Carneiro, 26-Apr-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) < 1) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘(𝐹‘𝑘)) ≤ (𝐴↑𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 0) | ||
| Theorem | geoserg 15959* | The value of the finite geometric series 𝐴↑𝑀 + 𝐴↑(𝑀 + 1) +... + 𝐴↑(𝑁 − 1). (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 1) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) = (((𝐴↑𝑀) − (𝐴↑𝑁)) / (1 − 𝐴))) | ||
| Theorem | geoser 15960* | The value of the finite geometric series 1 + 𝐴↑1 + 𝐴↑2 +... + 𝐴↑(𝑁 − 1). This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006.) (Proof shortened by Mario Carneiro, 15-Jun-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 1) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) = ((1 − (𝐴↑𝑁)) / (1 − 𝐴))) | ||
| Theorem | pwdif 15961* | The difference of two numbers to the same power is the difference of the two numbers multiplied with a finite sum. Generalization of subsq 14278. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 14278, 5-Aug-2021. (Contributed by AV, 6-Aug-2021.) (Revised by AV, 19-Aug-2021.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) | ||
| Theorem | pwm1geoser 15962* | The n-th power of a number decreased by 1 expressed by the finite geometric series 1 + 𝐴↑1 + 𝐴↑2 +... + 𝐴↑(𝑁 − 1). (Contributed by AV, 14-Aug-2021.) (Proof shortened by AV, 19-Aug-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘))) | ||
| Theorem | geolim 15963* | The partial sums in the infinite series 1 + 𝐴↑1 + 𝐴↑2... converge to (1 / (1 − 𝐴)). (Contributed by NM, 15-May-2006.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐴) < 1) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = (𝐴↑𝑘)) ⇒ ⊢ (𝜑 → seq0( + , 𝐹) ⇝ (1 / (1 − 𝐴))) | ||
| Theorem | geolim2 15964* | The partial sums in the geometric series 𝐴↑𝑀 + 𝐴↑(𝑀 + 1)... converge to ((𝐴↑𝑀) / (1 − 𝐴)). (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 26-Apr-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐴) < 1) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐴↑𝑘)) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ ((𝐴↑𝑀) / (1 − 𝐴))) | ||
| Theorem | georeclim 15965* | The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 1 < (abs‘𝐴)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = ((1 / 𝐴)↑𝑘)) ⇒ ⊢ (𝜑 → seq0( + , 𝐹) ⇝ (𝐴 / (𝐴 − 1))) | ||
| Theorem | geo2sum 15966* | The value of the finite geometric series 2↑-1 + 2↑-2 +... + 2↑-𝑁, multiplied by a constant. (Contributed by Mario Carneiro, 17-Mar-2014.) (Revised by Mario Carneiro, 26-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)(𝐴 / (2↑𝑘)) = (𝐴 − (𝐴 / (2↑𝑁)))) | ||
| Theorem | geo2sum2 15967* | The value of the finite geometric series 1 + 2 + 4 + 8 +... + 2↑(𝑁 − 1). (Contributed by Mario Carneiro, 7-Sep-2016.) |
| ⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (0..^𝑁)(2↑𝑘) = ((2↑𝑁) − 1)) | ||
| Theorem | geo2lim 15968* | The value of the infinite geometric series 2↑-1 + 2↑-2 +... , multiplied by a constant. (Contributed by Mario Carneiro, 15-Jun-2014.) |
| ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘))) ⇒ ⊢ (𝐴 ∈ ℂ → seq1( + , 𝐹) ⇝ 𝐴) | ||
| Theorem | geomulcvg 15969* | The geometric series converges even if it is multiplied by 𝑘 to result in the larger series 𝑘 · 𝐴↑𝑘. (Contributed by Mario Carneiro, 27-Mar-2015.) |
| ⊢ 𝐹 = (𝑘 ∈ ℕ0 ↦ (𝑘 · (𝐴↑𝑘))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , 𝐹) ∈ dom ⇝ ) | ||
| Theorem | geoisum 15970* | The infinite sum of 1 + 𝐴↑1 + 𝐴↑2... is (1 / (1 − 𝐴)). (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 26-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ0 (𝐴↑𝑘) = (1 / (1 − 𝐴))) | ||
| Theorem | geoisumr 15971* | The infinite sum of reciprocals 1 + (1 / 𝐴)↑1 + (1 / 𝐴)↑2... is 𝐴 / (𝐴 − 1). (Contributed by rpenner, 3-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 1 < (abs‘𝐴)) → Σ𝑘 ∈ ℕ0 ((1 / 𝐴)↑𝑘) = (𝐴 / (𝐴 − 1))) | ||
| Theorem | geoisum1 15972* | The infinite sum of 𝐴↑1 + 𝐴↑2... is (𝐴 / (1 − 𝐴)). (Contributed by NM, 1-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ (𝐴↑𝑘) = (𝐴 / (1 − 𝐴))) | ||
| Theorem | geoisum1c 15973* | The infinite sum of 𝐴 · (𝑅↑1) + 𝐴 · (𝑅↑2)... is (𝐴 · 𝑅) / (1 − 𝑅). (Contributed by NM, 2-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ (abs‘𝑅) < 1) → Σ𝑘 ∈ ℕ (𝐴 · (𝑅↑𝑘)) = ((𝐴 · 𝑅) / (1 − 𝑅))) | ||
| Theorem | 0.999... 15974 | The recurring decimal 0.999..., which is defined as the infinite sum 0.9 + 0.09 + 0.009 + ... i.e. 9 / 10↑1 + 9 / 10↑2 + 9 / 10↑3 + ..., is exactly equal to 1, according to ZF set theory. Interestingly, about 40% of the people responding to a poll at http://forum.physorg.com/index.php?showtopic=13177 disagree. (Contributed by NM, 2-Nov-2007.) (Revised by AV, 8-Sep-2021.) |
| ⊢ Σ𝑘 ∈ ℕ (9 / (;10↑𝑘)) = 1 | ||
| Theorem | geoihalfsum 15975 | Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 15972. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 15974 proves a similar claim for .999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.) (Proof shortened by AV, 9-Jul-2022.) |
| ⊢ Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1 | ||
| Theorem | cvgrat 15976* | Ratio test for convergence of a complex infinite series. If the ratio 𝐴 of the absolute values of successive terms in an infinite sequence 𝐹 is less than 1 for all terms beyond some index 𝐵, then the infinite sum of the terms of 𝐹 converges to a complex number. Equivalent to first part of Exercise 4 of [Gleason] p. 182. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 27-Apr-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) | ||
| Theorem | mertenslem1 15977* | Lemma for mertens 15979. (Contributed by Mario Carneiro, 29-Apr-2014.) |
| ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴) & ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) & ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗)))) & ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ ) & ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} & ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) & ⊢ (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))) & ⊢ (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) | ||
| Theorem | mertenslem2 15978* | Lemma for mertens 15979. (Contributed by Mario Carneiro, 28-Apr-2014.) |
| ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴) & ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) & ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗)))) & ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ ) & ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} & ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) | ||
| Theorem | mertens 15979* | Mertens' theorem. If 𝐴(𝑗) is an absolutely convergent series and 𝐵(𝑘) is convergent, then (Σ𝑗 ∈ ℕ0𝐴(𝑗) · Σ𝑘 ∈ ℕ0𝐵(𝑘)) = Σ𝑘 ∈ ℕ0Σ𝑗 ∈ (0...𝑘)(𝐴(𝑗) · 𝐵(𝑘 − 𝑗)) (and this latter series is convergent). This latter sum is commonly known as the Cauchy product of the sequences. The proof follows the outline at http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem. (Contributed by Mario Carneiro, 29-Apr-2014.) |
| ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴) & ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) & ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗)))) & ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ ) & ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵)) | ||
| Theorem | prodf 15980* | An infinite product of complex terms is a function from an upper set of integers to ℂ. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹):𝑍⟶ℂ) | ||
| Theorem | clim2prod 15981* | The limit of an infinite product with an initial segment added. (Contributed by Scott Fenton, 18-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ 𝐴) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘𝑁) · 𝐴)) | ||
| Theorem | clim2div 15982* | The limit of an infinite product with an initial segment removed. (Contributed by Scott Fenton, 20-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝐴) & ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0) ⇒ ⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ (𝐴 / (seq𝑀( · , 𝐹)‘𝑁))) | ||
| Theorem | prodfmul 15983* | The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , 𝐺)‘𝑁))) | ||
| Theorem | prodf1 15984 | The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (seq𝑀( · , (𝑍 × {1}))‘𝑁) = 1) | ||
| Theorem | prodf1f 15985 | A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) = (𝑍 × {1})) | ||
| Theorem | prodfclim1 15986 | The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) ⇝ 1) | ||
| Theorem | prodfn0 15987* | No term of a nonzero infinite product is zero. (Contributed by Scott Fenton, 14-Jan-2018.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ≠ 0) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0) | ||
| Theorem | prodfrec 15988* | The reciprocal of an infinite product. (Contributed by Scott Fenton, 15-Jan-2018.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) = (1 / (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) = (1 / (seq𝑀( · , 𝐹)‘𝑁))) | ||
| Theorem | prodfdiv 15989* | The quotient of two infinite products. (Contributed by Scott Fenton, 15-Jan-2018.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁))) | ||
| Theorem | ntrivcvg 15990* | A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) | ||
| Theorem | ntrivcvgn0 15991* | A product that converges to a nonzero value converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) | ||
| Theorem | ntrivcvgfvn0 15992* | Any value of a product sequence that converges to a nonzero value is itself nonzero. (Contributed by Scott Fenton, 20-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋) & ⊢ (𝜑 → 𝑋 ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0) | ||
| Theorem | ntrivcvgtail 15993* | A tail of a non-trivially convergent sequence converges non-trivially. (Contributed by Scott Fenton, 20-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋) & ⊢ (𝜑 → 𝑋 ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → (( ⇝ ‘seq𝑁( · , 𝐹)) ≠ 0 ∧ seq𝑁( · , 𝐹) ⇝ ( ⇝ ‘seq𝑁( · , 𝐹)))) | ||
| Theorem | ntrivcvgmullem 15994* | Lemma for ntrivcvgmul 15995. (Contributed by Scott Fenton, 19-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝑃 ∈ 𝑍) & ⊢ (𝜑 → 𝑋 ≠ 0) & ⊢ (𝜑 → 𝑌 ≠ 0) & ⊢ (𝜑 → seq𝑁( · , 𝐹) ⇝ 𝑋) & ⊢ (𝜑 → seq𝑃( · , 𝐺) ⇝ 𝑌) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ (𝜑 → 𝑁 ≤ 𝑃) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝑍 ∃𝑤(𝑤 ≠ 0 ∧ seq𝑞( · , 𝐻) ⇝ 𝑤)) | ||
| Theorem | ntrivcvgmul 15995* | The product of two non-trivially converging products converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → ∃𝑚 ∈ 𝑍 ∃𝑧(𝑧 ≠ 0 ∧ seq𝑚( · , 𝐺) ⇝ 𝑧)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ 𝑍 ∃𝑤(𝑤 ≠ 0 ∧ seq𝑝( · , 𝐻) ⇝ 𝑤)) | ||
| Syntax | cprod 15996 | Extend class notation to include complex products. |
| class ∏𝑘 ∈ 𝐴 𝐵 | ||
| Definition | df-prod 15997* | Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sum 15778 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) | ||
| Theorem | prodex 15998 | A product is a set. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ ∏𝑘 ∈ 𝐴 𝐵 ∈ V | ||
| Theorem | prodeq1f 15999 | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
| ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝐵 ⇒ ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | ||
| Theorem | prodeq1 16000* | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
| ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |