Home | Metamath
Proof Explorer Theorem List (p. 145 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | binom 14401* | 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 14400. 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 14402* | Special case of the binomial theorem for (1 + 𝐴)↑𝑁. (Contributed by Paul Chapman, 10-May-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((1 + 𝐴)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘))) | ||
Theorem | binom11 14403* | Special case of the binomial theorem for 2↑𝑁. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝑁 ∈ ℕ0 → (2↑𝑁) = Σ𝑘 ∈ (0...𝑁)(𝑁C𝑘)) | ||
Theorem | binom1dif 14404* | 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 14405 | Lemma for bcxmas 14406. (Contributed by Paul Chapman, 18-May-2007.) |
⊢ (𝐴 = 𝐵 → ((𝑁 + 𝐴)C𝐴) = ((𝑁 + 𝐵)C𝐵)) | ||
Theorem | bcxmas 14406* | 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 14407* | Lemma for incexc 14408. (Contributed by Mario Carneiro, 7-Aug-2017.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠)))) | ||
Theorem | incexc 14408* | 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 14409* | 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 14410* | Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝑗 = (𝐾 + 𝑘) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝑊 𝐴 = Σ𝑘 ∈ 𝑍 𝐵) | ||
Theorem | isumsplit 14411* | 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 14412* | 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 14413* | 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 14414* | 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 14415* | 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 14416* | A finite sum of nonnegative numbers is less or equal to its limit. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐵) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝑍 𝐵) | ||
Theorem | isumsup2 14417* | 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 14418* | 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 14419* | 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 14420* | Lemma for climcnds 14422: 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 14421* | Lemma for climcnds 14422: bound the condensed series by the original series. (Contributed by Mario Carneiro, 18-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁)))) | ||
Theorem | climcnds 14422* | 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.) |
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) ⇒ ⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq0( + , 𝐺) ∈ dom ⇝ )) | ||
Theorem | divrcnv 14423* | The sequence of reciprocals of real numbers, multiplied by the factor 𝐴, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℂ → (𝑛 ∈ ℝ+ ↦ (𝐴 / 𝑛)) ⇝𝑟 0) | ||
Theorem | divcnv 14424* | 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 14425 | The floor function satisfies ⌊(𝑥) = 𝑥 + 𝑂(1). (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ (𝑥 ∈ ℝ ↦ (𝑥 − (⌊‘𝑥))) ∈ 𝑂(1) | ||
Theorem | divcnvshft 14426* | Limit of a ratio function. (Contributed by Scott Fenton, 16-Dec-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐴 / (𝑘 + 𝐵))) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 0) | ||
Theorem | supcvg 14427* | 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 9140. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
⊢ 𝑋 ∈ V & ⊢ 𝑆 = sup(𝐴, ℝ, < ) & ⊢ 𝑅 = (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝐴) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹 ∘ 𝑓) ⇝ 𝑆)) | ||
Theorem | infcvgaux1i 14428* | Auxiliary theorem for applications of supcvg 14427. Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008.) |
⊢ 𝑅 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} & ⊢ (𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ) & ⊢ 𝑍 ∈ 𝑋 & ⊢ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 ⇒ ⊢ (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧) | ||
Theorem | infcvgaux2i 14429* | Auxiliary theorem for applications of supcvg 14427. (Contributed by NM, 4-Mar-2008.) |
⊢ 𝑅 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} & ⊢ (𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ) & ⊢ 𝑍 ∈ 𝑋 & ⊢ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 & ⊢ 𝑆 = -sup(𝑅, ℝ, < ) & ⊢ (𝑦 = 𝐶 → 𝐴 = 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑋 → 𝑆 ≤ 𝐵) | ||
Theorem | harmonic 14430 | The harmonic series 𝐻 diverges. This fact follows from the stronger emcl 24529, 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 14431* | 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 14432* | 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 14433 | Lemma for trirecip 14434. 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 14434 | 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 14435* | A sequence of powers of a complex number 𝐴 with absolute value smaller 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 14436* | A sequence of terms converges to zero when it is less than powers of a number 𝐴 whose absolute value is smaller than 1. (Contributed by NM, 19-Jul-2008.) (Revised by Mario Carneiro, 26-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) < 1) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘(𝐹‘𝑘)) ≤ (𝐴↑𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 0) | ||
Theorem | geoserg 14437* | The value of the finite geometric series 𝐴↑𝑀 + 𝐴↑(𝑀 + 1) +... + 𝐴↑(𝑁 − 1). (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 1) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) = (((𝐴↑𝑀) − (𝐴↑𝑁)) / (1 − 𝐴))) | ||
Theorem | geoser 14438* | 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 | pwm1geoser 14439* | 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.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘))) | ||
Theorem | geolim 14440* | 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 14441* | 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 14442* | 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 14443* | 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 14444* | 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 14445* | 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 14446* | 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 14447* | 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 14448* | 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 14449* | 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 14450* | 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... 14451 | 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 | 0.999...OLD 14452 | Obsolete version of 0.999... 14451 as of 8-Sep-2021. (Contributed by NM, 2-Nov-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Σ𝑘 ∈ ℕ (9 / (10↑𝑘)) = 1 | ||
Theorem | geoihalfsum 14453 | Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 14449. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 14451 proves a similar claim for .999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.) |
⊢ Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1 | ||
Theorem | cvgrat 14454* | 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 14455* | Lemma for mertens 14457. (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 14456* | Lemma for mertens 14457. (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 14457* | 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 14458* | 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 14459* | The limit of an infinite product with an initial segment added. (Contributed by Scott Fenton, 18-Dec-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ 𝐴) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘𝑁) · 𝐴)) | ||
Theorem | clim2div 14460* | 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 14461* | The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , 𝐺)‘𝑁))) | ||
Theorem | prodf1 14462 | The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (seq𝑀( · , (𝑍 × {1}))‘𝑁) = 1) | ||
Theorem | prodf1f 14463 | A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) = (𝑍 × {1})) | ||
Theorem | prodfclim1 14464 | The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) ⇝ 1) | ||
Theorem | prodfn0 14465* | No term of a nonzero infinite product is zero. (Contributed by Scott Fenton, 14-Jan-2018.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ≠ 0) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0) | ||
Theorem | prodfrec 14466* | The reciprocal of an infinite product. (Contributed by Scott Fenton, 15-Jan-2018.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) = (1 / (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) = (1 / (seq𝑀( · , 𝐹)‘𝑁))) | ||
Theorem | prodfdiv 14467* | The quotient of two infinite products. (Contributed by Scott Fenton, 15-Jan-2018.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁))) | ||
Theorem | ntrivcvg 14468* | A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) | ||
Theorem | ntrivcvgn0 14469* | A product that converges to a nonzero value converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) | ||
Theorem | ntrivcvgfvn0 14470* | 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 14471* | 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 14472* | Lemma for ntrivcvgmul 14473. (Contributed by Scott Fenton, 19-Dec-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝑃 ∈ 𝑍) & ⊢ (𝜑 → 𝑋 ≠ 0) & ⊢ (𝜑 → 𝑌 ≠ 0) & ⊢ (𝜑 → seq𝑁( · , 𝐹) ⇝ 𝑋) & ⊢ (𝜑 → seq𝑃( · , 𝐺) ⇝ 𝑌) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ (𝜑 → 𝑁 ≤ 𝑃) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝑍 ∃𝑤(𝑤 ≠ 0 ∧ seq𝑞( · , 𝐻) ⇝ 𝑤)) | ||
Theorem | ntrivcvgmul 14473* | 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 14474 | Extend class notation to include complex products. |
class ∏𝑘 ∈ 𝐴 𝐵 | ||
Definition | df-prod 14475* | Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sum 14265 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 14476 | A product is a set. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ ∏𝑘 ∈ 𝐴 𝐵 ∈ V | ||
Theorem | prodeq1f 14477 | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝐵 ⇒ ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | ||
Theorem | prodeq1 14478* | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | ||
Theorem | nfcprod1 14479* | Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ Ⅎ𝑘∏𝑘 ∈ 𝐴 𝐵 | ||
Theorem | nfcprod 14480* | 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 14481* | 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 14482* | 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 14483* | Equality theorem for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
Theorem | cbvprod 14484* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑘𝐵 & ⊢ Ⅎ𝑗𝐶 ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
Theorem | cbvprodv 14485* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
Theorem | cbvprodi 14486* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ Ⅎ𝑘𝐵 & ⊢ Ⅎ𝑗𝐶 & ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
Theorem | prodeq1i 14487* | Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶 | ||
Theorem | prodeq2i 14488* | Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝑘 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
Theorem | prodeq12i 14489* | Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑘 ∈ 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷 | ||
Theorem | prodeq1d 14490* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | ||
Theorem | prodeq2d 14491* | Equality deduction for product. Note that unlike prodeq2dv 14492, 𝑘 may occur in 𝜑. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
Theorem | prodeq2dv 14492* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
Theorem | prodeq2sdv 14493* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
Theorem | 2cprodeq2dv 14494* | Equality deduction for double product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐷) | ||
Theorem | prodeq12dv 14495* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) | ||
Theorem | prodeq12rdv 14496* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) | ||
Theorem | prod2id 14497* | 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 14498* | Lemma for prodrb 14501. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( · , 𝐹)) | ||
Theorem | fprodcvg 14499* | 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 14500* | Lemma for prodrb 14501. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (seq𝑀( · , 𝐹) ⇝ 𝐶 ↔ seq𝑁( · , 𝐹) ⇝ 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |