HomeTheorem List (p. 159 of 498)
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. 159 of 498) | < 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-30847) |
Hilbert Space Explorer
(30848-32370) |
Users' Mathboxes
(32371-49794) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bcxmas 15801* | 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 15802* | Lemma for incexc 15803. (Contributed by Mario Carneiro, 7-Aug-2017.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) | ||
| Theorem | incexc 15803* | 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 15804* | 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 15805* | Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝑗 = (𝐾 + 𝑘) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝑊 𝐴 = Σ𝑘 ∈ 𝑍 𝐵) | ||
| Theorem | isumsplit 15806* | 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 15807* | 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 15808* | 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 15809* | 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 15810* | 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 15811* | 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 15812* | 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 15813* | 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 15814* | 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 15815* | Lemma for climcnds 15817: 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 15816* | Lemma for climcnds 15817: 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 15817* | 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 15818* | The sequence of reciprocals of real numbers, multiplied by the factor 𝐴, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.) |
| ⊢ (𝐴 ∈ ℂ → (𝑛 ∈ ℝ+ ↦ (𝐴 / 𝑛)) ⇝𝑟 0) | ||
| Theorem | divcnv 15819* | 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 15820 | The floor function satisfies ⌊(𝑥) = 𝑥 + 𝑂(1). (Contributed by Mario Carneiro, 21-May-2016.) |
| ⊢ (𝑥 ∈ ℝ ↦ (𝑥 − (⌊‘𝑥))) ∈ 𝑂(1) | ||
| Theorem | divcnvshft 15821* | Limit of a ratio function. (Contributed by Scott Fenton, 16-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐴 / (𝑘 + 𝐵))) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 0) | ||
| Theorem | supcvg 15822* | 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 10388. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
| ⊢ 𝑋 ∈ V & ⊢ 𝑆 = sup(𝐴, ℝ, < ) & ⊢ 𝑅 = (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝐴) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹 ∘ 𝑓) ⇝ 𝑆)) | ||
| Theorem | infcvgaux1i 15823* | Auxiliary theorem for applications of supcvg 15822. Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008.) |
| ⊢ 𝑅 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} & ⊢ (𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ) & ⊢ 𝑍 ∈ 𝑋 & ⊢ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 ⇒ ⊢ (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧) | ||
| Theorem | infcvgaux2i 15824* | Auxiliary theorem for applications of supcvg 15822. (Contributed by NM, 4-Mar-2008.) |
| ⊢ 𝑅 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} & ⊢ (𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ) & ⊢ 𝑍 ∈ 𝑋 & ⊢ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 & ⊢ 𝑆 = -sup(𝑅, ℝ, < ) & ⊢ (𝑦 = 𝐶 → 𝐴 = 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑋 → 𝑆 ≤ 𝐵) | ||
| Theorem | harmonic 15825 | The harmonic series 𝐻 diverges. This fact follows from the stronger emcl 26913, 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 15826* | 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 15827* | 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 15828 | Lemma for trirecip 15829. 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 15829 | 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 15830* | 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 15831* | 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 15832* | The value of the finite geometric series 𝐴↑𝑀 + 𝐴↑(𝑀 + 1) +... + 𝐴↑(𝑁 − 1). (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 1) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) = (((𝐴↑𝑀) − (𝐴↑𝑁)) / (1 − 𝐴))) | ||
| Theorem | geoser 15833* | 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 15834* | The difference of two numbers to the same power is the difference of the two numbers multiplied with a finite sum. Generalization of subsq 14175. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 14175, 5-Aug-2021. (Contributed by AV, 6-Aug-2021.) (Revised by AV, 19-Aug-2021.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) | ||
| Theorem | pwm1geoser 15835* | 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 15836* | 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 15837* | 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 15838* | 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 15839* | 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 15840* | 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 15841* | 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 15842* | 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 15843* | 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 15844* | 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 15845* | 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 15846* | 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... 15847 | 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 15848 | Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 15845. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 15847 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 15849* | 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 15850* | Lemma for mertens 15852. (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 15851* | Lemma for mertens 15852. (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 15852* | 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 15853* | 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 15854* | The limit of an infinite product with an initial segment added. (Contributed by Scott Fenton, 18-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ 𝐴) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘𝑁) · 𝐴)) | ||
| Theorem | clim2div 15855* | 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 15856* | The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , 𝐺)‘𝑁))) | ||
| Theorem | prodf1 15857 | The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (seq𝑀( · , (𝑍 × {1}))‘𝑁) = 1) | ||
| Theorem | prodf1f 15858 | A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) = (𝑍 × {1})) | ||
| Theorem | prodfclim1 15859 | The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) ⇝ 1) | ||
| Theorem | prodfn0 15860* | No term of a nonzero infinite product is zero. (Contributed by Scott Fenton, 14-Jan-2018.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ≠ 0) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0) | ||
| Theorem | prodfrec 15861* | The reciprocal of an infinite product. (Contributed by Scott Fenton, 15-Jan-2018.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) = (1 / (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) = (1 / (seq𝑀( · , 𝐹)‘𝑁))) | ||
| Theorem | prodfdiv 15862* | The quotient of two infinite products. (Contributed by Scott Fenton, 15-Jan-2018.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁))) | ||
| Theorem | ntrivcvg 15863* | A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) | ||
| Theorem | ntrivcvgn0 15864* | A product that converges to a nonzero value converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) | ||
| Theorem | ntrivcvgfvn0 15865* | 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 15866* | 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 15867* | Lemma for ntrivcvgmul 15868. (Contributed by Scott Fenton, 19-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝑃 ∈ 𝑍) & ⊢ (𝜑 → 𝑋 ≠ 0) & ⊢ (𝜑 → 𝑌 ≠ 0) & ⊢ (𝜑 → seq𝑁( · , 𝐹) ⇝ 𝑋) & ⊢ (𝜑 → seq𝑃( · , 𝐺) ⇝ 𝑌) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ (𝜑 → 𝑁 ≤ 𝑃) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝑍 ∃𝑤(𝑤 ≠ 0 ∧ seq𝑞( · , 𝐻) ⇝ 𝑤)) | ||
| Theorem | ntrivcvgmul 15868* | 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 15869 | Extend class notation to include complex products. |
| class ∏𝑘 ∈ 𝐴 𝐵 | ||
| Definition | df-prod 15870* | Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sum 15653 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 15871 | A product is a set. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ ∏𝑘 ∈ 𝐴 𝐵 ∈ V | ||
| Theorem | prodeq1f 15872 | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
| ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝐵 ⇒ ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | ||
| Theorem | prodeq1 15873* | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
| ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | ||
| Theorem | nfcprod1 15874* | Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ Ⅎ𝑘𝐴 ⇒ ⊢ Ⅎ𝑘∏𝑘 ∈ 𝐴 𝐵 | ||
| Theorem | nfcprod 15875* | Bound-variable hypothesis builder for product: if 𝑥 is (effectively) not free in 𝐴 and 𝐵, it is not free in ∏𝑘 ∈ 𝐴𝐵. (Contributed by Scott Fenton, 1-Dec-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥∏𝑘 ∈ 𝐴 𝐵 | ||
| Theorem | prodeq2w 15876* | Equality theorem for product, when the class expressions 𝐵 and 𝐶 are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (∀𝑘 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
| Theorem | prodeq2ii 15877* | Equality theorem for product, with the class expressions 𝐵 and 𝐶 guarded by I to be always sets. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
| Theorem | prodeq2 15878* | Equality theorem for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
| Theorem | cbvprod 15879* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑘𝐵 & ⊢ Ⅎ𝑗𝐶 ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
| Theorem | cbvprodv 15880* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
| Theorem | cbvprodi 15881* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ Ⅎ𝑘𝐵 & ⊢ Ⅎ𝑗𝐶 & ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
| Theorem | prodeq1i 15882 | Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.) Remove DV conditions. (Revised by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶 | ||
| Theorem | prodeq1iOLD 15883* | Obsolete version of prodeq1i 15882 as of 1-Sep-2025. (Contributed by Scott Fenton, 4-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶 | ||
| Theorem | prodeq2i 15884* | Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (𝑘 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
| Theorem | prodeq12i 15885* | Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝑘 ∈ 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷 | ||
| Theorem | prodeq1d 15886* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | ||
| Theorem | prodeq2d 15887* | Equality deduction for product. Note that unlike prodeq2dv 15888, 𝑘 may occur in 𝜑. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
| Theorem | prodeq2dv 15888* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
| Theorem | prodeq2sdv 15889* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) Avoid axioms. (Revised by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
| Theorem | prodeq2sdvOLD 15890* | Obsolete version of prodeq2sdv 15889 as of 1-Sep-2025. (Contributed by Scott Fenton, 4-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
| Theorem | 2cprodeq2dv 15891* | Equality deduction for double product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐷) | ||
| Theorem | prodeq12dv 15892* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) | ||
| Theorem | prodeq12rdv 15893* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) | ||
| Theorem | prod2id 15894* | The second class argument to a product can be chosen so that it is always a set. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 ( I ‘𝐵) | ||
| Theorem | prodrblem 15895* | Lemma for prodrb 15898. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( · , 𝐹)) | ||
| Theorem | fprodcvg 15896* | The sequence of partial products of a finite product converges to the whole product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘𝑁)) | ||
| Theorem | prodrblem2 15897* | Lemma for prodrb 15898. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (seq𝑀( · , 𝐹) ⇝ 𝐶 ↔ seq𝑁( · , 𝐹) ⇝ 𝐶)) | ||
| Theorem | prodrb 15898* | Rebase the starting point of a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑁)) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐹) ⇝ 𝐶 ↔ seq𝑁( · , 𝐹) ⇝ 𝐶)) | ||
| Theorem | prodmolem3 15899* | Lemma for prodmo 15902. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑘⦌𝐵) & ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ ⦋(𝐾‘𝑗) / 𝑘⦌𝐵) & ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) & ⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) ⇒ ⊢ (𝜑 → (seq1( · , 𝐺)‘𝑀) = (seq1( · , 𝐻)‘𝑁)) | ||
| Theorem | prodmolem2a 15900* | Lemma for prodmo 15902. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑘⦌𝐵) & ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ ⦋(𝐾‘𝑗) / 𝑘⦌𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴)) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |