P. 121 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12001-12100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fzosump1 12001*	Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (𝑀..^𝑁)𝐴 + 𝐵))
Theorem	fsum1p 12002*	Separate out the first term in a finite sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (𝐵 + Σ𝑘 ∈ ((𝑀 + 1)...𝑁)𝐴))
Theorem	fsumsplitsnun 12003*	Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by AV, 17-Dec-2021.)
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 = (Σ𝑘 ∈ 𝐴 𝐵 + ⦋𝑍 / 𝑘⦌𝐵))
Theorem	fsump1 12004*	The addition of the next term in a finite sum of 𝐴(𝑘) is the current term plus 𝐵 i.e. 𝐴(𝑁 + 1). (Contributed by NM, 4-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (𝑀...𝑁)𝐴 + 𝐵))
Theorem	isumclim 12005*	An infinite sum equals the value its series converges to. (Contributed by NM, 25-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = 𝐵)
Theorem	isumclim2 12006*	A converging series converges to its infinite sum. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ Σ𝑘 ∈ 𝑍 𝐴)
Theorem	isumclim3 12007*	The sequence of partial finite sums of a converging infinite series converges to the infinite sum of the series. Note that 𝑗 must not occur in 𝐴. (Contributed by NM, 9-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = Σ𝑘 ∈ (𝑀...𝑗)𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ Σ𝑘 ∈ 𝑍 𝐴)
Theorem	sumnul 12008*	The sum of a non-convergent infinite series evaluates to the empty set. (Contributed by Paul Chapman, 4-Nov-2007.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = ∅)
Theorem	isumcl 12009*	The sum of a converging infinite series is a complex number. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℂ)
Theorem	isummulc2 12010*	An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐵 · Σ𝑘 ∈ 𝑍 𝐴) = Σ𝑘 ∈ 𝑍 (𝐵 · 𝐴))
Theorem	isummulc1 12011*	An infinite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝑍 𝐴 · 𝐵) = Σ𝑘 ∈ 𝑍 (𝐴 · 𝐵))
Theorem	isumdivapc 12012*	An infinite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝑍 𝐴 / 𝐵) = Σ𝑘 ∈ 𝑍 (𝐴 / 𝐵))
Theorem	isumrecl 12013*	The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℝ)
Theorem	isumge0 12014*	An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ 𝑍 𝐴)
Theorem	isumadd 12015*	Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 (𝐴 + 𝐵) = (Σ𝑘 ∈ 𝑍 𝐴 + Σ𝑘 ∈ 𝑍 𝐵))
Theorem	sumsplitdc 12016*	Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → DECID 𝑘 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → DECID 𝑘 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐶, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = if(𝑘 ∈ 𝐵, 𝐶, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∪ 𝐵)) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶))
Theorem	fsump1i 12017*	Optimized version of fsump1 12004 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑁 = (𝐾 + 1)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝐾)𝐴 = 𝑆))    &   ⊢ (𝜑 → (𝑆 + 𝐵) = 𝑇)    ⇒   ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝑁)𝐴 = 𝑇))
Theorem	fsum2dlemstep 12018*	Lemma for fsum2d 12019- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.)
⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ¬ 𝑦 ∈ 𝑥)    &   ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑥 ∈ Fin)    &   ⊢ (𝜓 ↔ Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)
Theorem	fsum2d 12019*	Write a double sum as a sum over a two-dimensional region. Note that 𝐵(𝑗) is a function of 𝑗. (Contributed by Mario Carneiro, 27-Apr-2014.)
⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷)
Theorem	fsumxp 12020*	Combine two sums into a single sum over the cartesian product. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ (𝐴 × 𝐵)𝐷)
Theorem	fsumcnv 12021*	Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ (𝑥 = ⟨𝑗, 𝑘⟩ → 𝐵 = 𝐷)    &   ⊢ (𝑦 = ⟨𝑘, 𝑗⟩ → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → Rel 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑦 ∈ ◡ 𝐴𝐶)
Theorem	fisumcom2 12022*	Interchange order of summation. Note that 𝐵(𝑗) and 𝐷(𝑘) are not necessarily constant expressions. (Contributed by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.) (Proof shortened by JJ, 2-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷)))    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐸 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐸 = Σ𝑘 ∈ 𝐶 Σ𝑗 ∈ 𝐷 𝐸)
Theorem	fsumcom 12023*	Interchange order of summation. (Contributed by NM, 15-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝐵 Σ𝑗 ∈ 𝐴 𝐶)
Theorem	fsum0diaglem 12024*	Lemma for fisum0diag 12025. (Contributed by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.)
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑘 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 𝑘))))
Theorem	fisum0diag 12025*	Two ways to express "the sum of 𝐴(𝑗, 𝑘) over the triangular region 𝑀 ≤ 𝑗, 𝑀 ≤ 𝑘, 𝑗 + 𝑘 ≤ 𝑁". (Contributed by NM, 31-Dec-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.)
⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗)))) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)Σ𝑘 ∈ (0...(𝑁 − 𝑗))𝐴 = Σ𝑘 ∈ (0...𝑁)Σ𝑗 ∈ (0...(𝑁 − 𝑘))𝐴)
Theorem	mptfzshft 12026*	1-1 onto function in maps-to notation which shifts a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)):((𝑀 + 𝐾)...(𝑁 + 𝐾))–1-1-onto→(𝑀...𝑁))
Theorem	fsumrev 12027*	Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑗 = (𝐾 − 𝑘) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝐵)
Theorem	fsumshft 12028*	Index shift of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) (Proof shortened by AV, 8-Sep-2019.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑗 = (𝑘 − 𝐾) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵)
Theorem	fsumshftm 12029*	Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑗 = (𝑘 + 𝐾) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾))𝐵)
Theorem	fisumrev2 12030*	Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 13-Apr-2016.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑗 = ((𝑀 + 𝑁) − 𝑘) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ (𝑀...𝑁)𝐵)
Theorem	fisum0diag2 12031*	Two ways to express "the sum of 𝐴(𝑗, 𝑘) over the triangular region 0 ≤ 𝑗, 0 ≤ 𝑘, 𝑗 + 𝑘 ≤ 𝑁". (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐴)    &   ⊢ (𝑥 = (𝑘 − 𝑗) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗)))) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)Σ𝑘 ∈ (0...(𝑁 − 𝑗))𝐴 = Σ𝑘 ∈ (0...𝑁)Σ𝑗 ∈ (0...𝑘)𝐶)
Theorem	fsummulc2 12032*	A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶 · Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐶 · 𝐵))
Theorem	fsummulc1 12033*	A finite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 · 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶))
Theorem	fsumdivapc 12034*	A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 / 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 / 𝐶))
Theorem	fsumneg 12035*	Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -𝐵 = -Σ𝑘 ∈ 𝐴 𝐵)
Theorem	fsumsub 12036*	Split a finite sum over a subtraction. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 − 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 − Σ𝑘 ∈ 𝐴 𝐶))
Theorem	fsum2mul 12037*	Separate the nested sum of the product 𝐶(𝑗) · 𝐷(𝑘). (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 (𝐶 · 𝐷) = (Σ𝑗 ∈ 𝐴 𝐶 · Σ𝑘 ∈ 𝐵 𝐷))
Theorem	fsumconst 12038*	The sum of constant terms (𝑘 is not free in 𝐵). (Contributed by NM, 24-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵))
Theorem	fsumdifsnconst 12039*	The sum of constant terms (𝑘 is not free in 𝐶) over an index set excluding a singleton. (Contributed by AV, 7-Jan-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ ℂ) → Σ𝑘 ∈ (𝐴 ∖ {𝐵})𝐶 = (((♯‘𝐴) − 1) · 𝐶))
Theorem	modfsummodlem1 12040*	Lemma for modfsummod 12042. (Contributed by Alexander van der Vekens, 1-Sep-2018.)
⊢ (∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ)
Theorem	modfsummodlemstep 12041*	Induction step for modfsummod 12042. (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by Jim Kingdon, 12-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 mod 𝑁) = (Σ𝑘 ∈ 𝐴 (𝐵 mod 𝑁) mod 𝑁))    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 mod 𝑁) = (Σ𝑘 ∈ (𝐴 ∪ {𝑧})(𝐵 mod 𝑁) mod 𝑁))
Theorem	modfsummod 12042*	A finite sum modulo a positive integer equals the finite sum of their summands modulo the positive integer, modulo the positive integer. (Contributed by Alexander van der Vekens, 1-Sep-2018.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 mod 𝑁) = (Σ𝑘 ∈ 𝐴 (𝐵 mod 𝑁) mod 𝑁))
Theorem	fsumge0 12043*	If all of the terms of a finite sum are nonnegative, so is the sum. (Contributed by NM, 26-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ 𝐴 𝐵)
Theorem	fsumlessfi 12044*	A shorter sum of nonnegative terms is no greater than a longer one. (Contributed by NM, 26-Dec-2005.) (Revised by Jim Kingdon, 12-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵)
Theorem	fsumge1 12045*	A sum of nonnegative numbers is greater than or equal to any one of its terms. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 4-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)    &   ⊢ (𝑘 = 𝑀 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ≤ Σ𝑘 ∈ 𝐴 𝐵)
Theorem	fsum00 12046*	A sum of nonnegative numbers is zero iff all terms are zero. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 = 0 ↔ ∀𝑘 ∈ 𝐴 𝐵 = 0))
Theorem	fsumle 12047*	If all of the terms of finite sums compare, so do the sums. (Contributed by NM, 11-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐶)
Theorem	fsumlt 12048*	If every term in one finite sum is less than the corresponding term in another, then the first sum is less than the second. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 < Σ𝑘 ∈ 𝐴 𝐶)
Theorem	fsumabs 12049*	Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘Σ𝑘 ∈ 𝐴 𝐵) ≤ Σ𝑘 ∈ 𝐴 (abs‘𝐵))
Theorem	telfsumo 12050*	Sum of a telescoping series, using half-open intervals. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵)    &   ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐸)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 − 𝐶) = (𝐷 − 𝐸))
Theorem	telfsumo2 12051*	Sum of a telescoping series. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵)    &   ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐸)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 − 𝐵) = (𝐸 − 𝐷))
Theorem	telfsum 12052*	Sum of a telescoping series. (Contributed by Scott Fenton, 24-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.)
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵)    &   ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷)    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐸)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)(𝐵 − 𝐶) = (𝐷 − 𝐸))
Theorem	telfsum2 12053*	Sum of a telescoping series. (Contributed by Mario Carneiro, 15-Jun-2014.) (Revised by Mario Carneiro, 2-May-2016.)
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵)    &   ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷)    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐸)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)(𝐶 − 𝐵) = (𝐸 − 𝐷))
Theorem	fsumparts 12054*	Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (𝑘 = 𝑗 → (𝐴 = 𝐵 ∧ 𝑉 = 𝑊))    &   ⊢ (𝑘 = (𝑗 + 1) → (𝐴 = 𝐶 ∧ 𝑉 = 𝑋))    &   ⊢ (𝑘 = 𝑀 → (𝐴 = 𝐷 ∧ 𝑉 = 𝑌))    &   ⊢ (𝑘 = 𝑁 → (𝐴 = 𝐸 ∧ 𝑉 = 𝑍))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑉 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊)) = (((𝐸 · 𝑍) − (𝐷 · 𝑌)) − Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋)))
Theorem	fsumrelem 12055*	Lemma for fsumre 12056, fsumim 12057, and fsumcj 12058. (Contributed by Mario Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐹:ℂ⟶ℂ    &   ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) + (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵))
Theorem	fsumre 12056*	The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (ℜ‘𝐵))
Theorem	fsumim 12057*	The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (ℑ‘𝐵))
Theorem	fsumcj 12058*	The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (∗‘𝐵))
Theorem	iserabs 12059*	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 Jim Kingdon, 14-Dec-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)    &   ⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → (abs‘𝐴) ≤ 𝐵)
Theorem	cvgcmpub 12060*	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	fsumiun 12061*	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 12062*	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 12063*	The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Fin)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Disj 𝑦 ∈ 𝐵 𝐶)    ⇒   ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) = Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 (♯‘𝐶))
Theorem	hash2iun1dif1 12064*	The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ 𝐵 = (𝐴 ∖ {𝑥})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Fin)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Disj 𝑦 ∈ 𝐵 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (♯‘𝐶) = 1)    ⇒   ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) = ((♯‘𝐴) · ((♯‘𝐴) − 1)))
Theorem	hashrabrex 12065*	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 12066*	The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ Fin)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥)    ⇒   ⊢ (𝜑 → (♯‘∪ 𝐴) = Σ𝑥 ∈ 𝐴 (♯‘𝑥))
4.9.3  The binomial theorem
Theorem	binomlem 12067*	Lemma for binom 12068 (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 12068*	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 12067. 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 12069*	Special case of the binomial theorem for (1 + 𝐴)↑𝑁. (Contributed by Paul Chapman, 10-May-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((1 + 𝐴)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘)))
Theorem	binom11 12070*	Special case of the binomial theorem for 2↑𝑁. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝑁 ∈ ℕ0 → (2↑𝑁) = Σ𝑘 ∈ (0...𝑁)(𝑁C𝑘))
Theorem	binom1dif 12071*	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 12072	Lemma for bcxmas 12073. (Contributed by Paul Chapman, 18-May-2007.)
⊢ (𝐴 = 𝐵 → ((𝑁 + 𝐴)C𝐴) = ((𝑁 + 𝐵)C𝐵))
Theorem	bcxmas 12073*	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𝑗))
4.9.4  Infinite sums (cont.)
Theorem	isumshft 12074*	Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾))    &   ⊢ (𝑗 = (𝐾 + 𝑘) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝑊 𝐴 = Σ𝑘 ∈ 𝑍 𝐵)
Theorem	isumsplit 12075*	Split off the first 𝑁 terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 21-Oct-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴))
Theorem	isum1p 12076*	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 12077*	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 12078*	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 12079*	Comparison of two infinite sums. (Contributed by Paul Chapman, 13-Nov-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ≤ Σ𝑘 ∈ 𝑍 𝐵)
Theorem	isumlessdc 12080*	A finite sum of nonnegative numbers is less than or equal to its limit. (Contributed by Mario Carneiro, 24-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 DECID 𝑘 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐵)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝑍 𝐵)
4.9.5  Miscellaneous converging and diverging sequences
Theorem	divcnv 12081*	The sequence of reciprocals of positive integers, multiplied by the factor 𝐴, converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Jim Kingdon, 22-Oct-2022.)
⊢ (𝐴 ∈ ℂ → (𝑛 ∈ ℕ ↦ (𝐴 / 𝑛)) ⇝ 0)
4.9.6  Arithmetic series
Theorem	arisum 12082*	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 12083*	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 12084	Lemma for trirecip 12085. 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 12085	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
4.9.7  Geometric series
Theorem	expcnvap0 12086*	A sequence of powers of a complex number 𝐴 with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 23-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝐴) < 1)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0)
Theorem	expcnvre 12087*	A sequence of powers of a nonnegative real number less than one converges to zero. (Contributed by Jim Kingdon, 28-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0)
Theorem	expcnv 12088*	A sequence of powers of a complex number 𝐴 with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 28-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝐴) < 1)    ⇒   ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0)
Theorem	explecnv 12089*	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	geosergap 12090*	The value of the finite geometric series 𝐴↑𝑀 + 𝐴↑(𝑀 + 1) +... + 𝐴↑(𝑁 − 1). (Contributed by Mario Carneiro, 2-May-2016.) (Revised by Jim Kingdon, 24-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 1)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) = (((𝐴↑𝑀) − (𝐴↑𝑁)) / (1 − 𝐴)))
Theorem	geoserap 12091*	The value of the finite geometric series 1 + 𝐴↑1 + 𝐴↑2 +... + 𝐴↑(𝑁 − 1). This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006.) (Revised by Jim Kingdon, 24-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 1)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) = ((1 − (𝐴↑𝑁)) / (1 − 𝐴)))
Theorem	pwm1geoserap1 12092*	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.) (Revised by Jim Kingdon, 24-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 # 1)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))
Theorem	absltap 12093	Less-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐴) < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 # 𝐵)
Theorem	absgtap 12094	Greater-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 < (abs‘𝐴))    ⇒   ⊢ (𝜑 → 𝐴 # 𝐵)
Theorem	geolim 12095*	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 12096*	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 12097*	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 12098*	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 12099*	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 12100*	The value of the infinite geometric series 2↑-1 + 2↑-2 +... , multiplied by a constant. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘)))    ⇒   ⊢ (𝐴 ∈ ℂ → seq1( + , 𝐹) ⇝ 𝐴)