P. 114 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11301-11400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cbvsum 11301	Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ Ⅎ𝑗𝐶    ⇒   ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	cbvsumv 11302*	Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    ⇒   ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	cbvsumi 11303*	Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
⊢ Ⅎ𝑘𝐵    &   ⊢ Ⅎ𝑗𝐶    &   ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    ⇒   ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	sumeq1i 11304*	Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶
Theorem	sumeq2i 11305*	Equality inference for sum. (Contributed by NM, 3-Dec-2005.)
⊢ (𝑘 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	sumeq12i 11306*	Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑘 ∈ 𝐴 → 𝐶 = 𝐷)    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷
Theorem	sumeq1d 11307*	Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
Theorem	sumeq2d 11308*	Equality deduction for sum. Note that unlike sumeq2dv 11309, 𝑘 may occur in 𝜑. (Contributed by NM, 1-Nov-2005.)
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	sumeq2dv 11309*	Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	sumeq2ad 11310*	Equality deduction for sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	sumeq2sdv 11311*	Equality deduction for sum. (Contributed by NM, 3-Jan-2006.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	2sumeq2dv 11312*	Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐷)
Theorem	sumeq12dv 11313*	Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	sumeq12rdv 11314*	Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	sumfct 11315*	A lemma to facilitate conversions from the function form to the class-variable form of a sum. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 18-Sep-2022.)
⊢ (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → Σ𝑗 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	fz1f1o 11316*	A lemma for working with finite sums. (Contributed by Mario Carneiro, 22-Apr-2014.)
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
Theorem	nnf1o 11317	Lemma for sum and product theorems. (Contributed by Jim Kingdon, 15-Aug-2022.)
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ))    &   ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐺:(1...𝑁)–1-1-onto→𝐴)    ⇒   ⊢ (𝜑 → 𝑁 = 𝑀)
Theorem	sumrbdclem 11318*	Lemma for sumrbdc 11320. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 8-Apr-2023.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( + , 𝐹))
Theorem	fsum3cvg 11319*	The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 12-Nov-2022.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁))
Theorem	sumrbdc 11320*	Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑁))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → DECID 𝑘 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹) ⇝ 𝐶 ↔ seq𝑁( + , 𝐹) ⇝ 𝐶))
Theorem	summodclem3 11321*	Lemma for summodc 11324. (Contributed by Mario Carneiro, 29-Mar-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ))    &   ⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0))    ⇒   ⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁))
Theorem	summodclem2a 11322*	Lemma for summodc 11324. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))
Theorem	summodclem2 11323*	Lemma for summodc 11324. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))    ⇒   ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
Theorem	summodc 11324*	A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))    ⇒   ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))))
Theorem	zsumdc 11325*	Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) (Revised by Jim Kingdon, 8-Apr-2023.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑍 DECID 𝑥 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( + , 𝐹)))
Theorem	isum 11326*	Series sum with an upper integer index set (i.e. an infinite series). (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario Carneiro, 7-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐵 = ( ⇝ ‘seq𝑀( + , 𝐹)))
Theorem	fsumgcl 11327*	Closure for a function used to describe a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.)
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶)    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
Theorem	fsum3 11328*	The value of a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.)
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))
Theorem	sum0 11329	Any sum over the empty set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
⊢ Σ𝑘 ∈ ∅ 𝐴 = 0
Theorem	isumz 11330*	Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ (ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∨ 𝐴 ∈ Fin) → Σ𝑘 ∈ 𝐴 0 = 0)
Theorem	fsumf1o 11331*	Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014.)
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)
Theorem	isumss 11332*	Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 21-Sep-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)    &   ⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ⊆ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
Theorem	fisumss 11333*	Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)    &   ⊢ (𝜑 → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
Theorem	isumss2 11334*	Change the index set of a sum by adding zeroes. The nonzero elements are in the contained set 𝐴 and the added zeroes compose the rest of the containing set 𝐵 which needs to be summable. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Jim Kingdon, 24-Sep-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ((𝑀 ∈ ℤ ∧ 𝐵 ⊆ (ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐵) ∨ 𝐵 ∈ Fin))    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 if(𝑘 ∈ 𝐴, 𝐶, 0))
Theorem	fsum3cvg2 11335*	The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁))
Theorem	fsumsersdc 11336*	Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Jim Kingdon, 5-May-2023.)
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq𝑀( + , 𝐹)‘𝑁))
Theorem	fsum3cvg3 11337*	A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Theorem	fsum3ser 11338*	A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 11353 and fsump1 11361, which should make our notation clear and from which, along with closure fsumcl 11341, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.)
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( + , 𝐹)‘𝑁))
Theorem	fsumcl2lem 11339*	- Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.) (Contributed by Mario Carneiro, 3-Jun-2014.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	fsumcllem 11340*	- Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.) (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 3-Jun-2014.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 0 ∈ 𝑆)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	fsumcl 11341*	Closure of a finite sum of complex numbers 𝐴(𝑘). (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
Theorem	fsumrecl 11342*	Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)
Theorem	fsumzcl 11343*	Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℤ)
Theorem	fsumnn0cl 11344*	Closure of a finite sum of nonnegative integers. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℕ0)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ0)
Theorem	fsumrpcl 11345*	Closure of a finite sum of positive reals. (Contributed by Mario Carneiro, 3-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ+)
Theorem	fsumzcl2 11346*	A finite sum with integer summands is an integer. (Contributed by Alexander van der Vekens, 31-Aug-2018.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℤ)
Theorem	fsumadd 11347*	The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))
Theorem	fsumsplit 11348*	Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.)
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶))
Theorem	fsumsplitf 11349*	Split a sum into two parts. A version of fsumsplit 11348 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶))
Theorem	sumsnf 11350*	A sum of a singleton is the term. A version of sumsn 11352 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝐵    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	fsumsplitsn 11351*	Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐷    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∪ {𝐵})𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + 𝐷))
Theorem	sumsn 11352*	A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.)
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	fsum1 11353*	The finite sum of 𝐴(𝑘) from 𝑘 = 𝑀 to 𝑀 (i.e. a sum with only one term) is 𝐵 i.e. 𝐴(𝑀). (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (𝑀...𝑀)𝐴 = 𝐵)
Theorem	sumpr 11354*	A sum over a pair is the sum of the elements. (Contributed by Thierry Arnoux, 12-Dec-2016.)
⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸)    &   ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ))    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 + 𝐸))
Theorem	sumtp 11355*	A sum over a triple is the sum of the elements. (Contributed by AV, 24-Jul-2020.)
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸)    &   ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹)    &   ⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺)    &   ⊢ (𝜑 → (𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ))    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 + 𝐹) + 𝐺))
Theorem	sumsns 11356*	A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.)
⊢ ((𝑀 ∈ 𝑉 ∧ ⦋𝑀 / 𝑘⦌𝐴 ∈ ℂ) → Σ𝑘 ∈ {𝑀}𝐴 = ⦋𝑀 / 𝑘⦌𝐴)
Theorem	fsumm1 11357*	Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 26-Apr-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + 𝐵))
Theorem	fzosump1 11358*	Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (𝑀..^𝑁)𝐴 + 𝐵))
Theorem	fsum1p 11359*	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 11360*	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 11361*	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 11362*	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 11363*	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 11364*	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 11365*	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 11366*	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 11367*	An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐵 · Σ𝑘 ∈ 𝑍 𝐴) = Σ𝑘 ∈ 𝑍 (𝐵 · 𝐴))
Theorem	isummulc1 11368*	An infinite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝑍 𝐴 · 𝐵) = Σ𝑘 ∈ 𝑍 (𝐴 · 𝐵))
Theorem	isumdivapc 11369*	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 11370*	The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℝ)
Theorem	isumge0 11371*	An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ 𝑍 𝐴)
Theorem	isumadd 11372*	Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 (𝐴 + 𝐵) = (Σ𝑘 ∈ 𝑍 𝐴 + Σ𝑘 ∈ 𝑍 𝐵))
Theorem	sumsplitdc 11373*	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 11374*	Optimized version of fsump1 11361 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑁 = (𝐾 + 1)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝐾)𝐴 = 𝑆))    &   ⊢ (𝜑 → (𝑆 + 𝐵) = 𝑇)    ⇒   ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝑁)𝐴 = 𝑇))
Theorem	fsum2dlemstep 11375*	Lemma for fsum2d 11376- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.)
⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ¬ 𝑦 ∈ 𝑥)    &   ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑥 ∈ Fin)    &   ⊢ (𝜓 ↔ Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)
Theorem	fsum2d 11376*	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 11377*	Combine two sums into a single sum over the cartesian product. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ (𝐴 × 𝐵)𝐷)
Theorem	fsumcnv 11378*	Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ (𝑥 = ⟨𝑗, 𝑘⟩ → 𝐵 = 𝐷)    &   ⊢ (𝑦 = ⟨𝑘, 𝑗⟩ → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → Rel 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑦 ∈ ◡ 𝐴𝐶)
Theorem	fisumcom2 11379*	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 11380*	Interchange order of summation. (Contributed by NM, 15-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝐵 Σ𝑗 ∈ 𝐴 𝐶)
Theorem	fsum0diaglem 11381*	Lemma for fisum0diag 11382. (Contributed by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.)
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑘 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 𝑘))))
Theorem	fisum0diag 11382*	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 11383*	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 11384*	Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑗 = (𝐾 − 𝑘) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝐵)
Theorem	fsumshft 11385*	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 11386*	Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑗 = (𝑘 + 𝐾) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾))𝐵)
Theorem	fisumrev2 11387*	Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 13-Apr-2016.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑗 = ((𝑀 + 𝑁) − 𝑘) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ (𝑀...𝑁)𝐵)
Theorem	fisum0diag2 11388*	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 11389*	A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶 · Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐶 · 𝐵))
Theorem	fsummulc1 11390*	A finite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 · 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶))
Theorem	fsumdivapc 11391*	A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 / 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 / 𝐶))
Theorem	fsumneg 11392*	Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -𝐵 = -Σ𝑘 ∈ 𝐴 𝐵)
Theorem	fsumsub 11393*	Split a finite sum over a subtraction. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 − 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 − Σ𝑘 ∈ 𝐴 𝐶))
Theorem	fsum2mul 11394*	Separate the nested sum of the product 𝐶(𝑗) · 𝐷(𝑘). (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 (𝐶 · 𝐷) = (Σ𝑗 ∈ 𝐴 𝐶 · Σ𝑘 ∈ 𝐵 𝐷))
Theorem	fsumconst 11395*	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 11396*	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 11397*	Lemma for modfsummod 11399. (Contributed by Alexander van der Vekens, 1-Sep-2018.)
⊢ (∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ)
Theorem	modfsummodlemstep 11398*	Induction step for modfsummod 11399. (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 11399*	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 11400*	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 ≤ Σ𝑘 ∈ 𝐴 𝐵)