P. 157 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15601-15700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	climaddc1 15601*	Limit of a constant 𝐶 added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = ((𝐹‘𝑘) + 𝐶))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (𝐴 + 𝐶))
Theorem	climaddc2 15602*	Limit of a constant 𝐶 added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐶 + (𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (𝐶 + 𝐴))
Theorem	climmulc2 15603*	Limit of a sequence multiplied by a constant 𝐶. Corollary 12-2.2 of [Gleason] p. 171. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐶 · (𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (𝐶 · 𝐴))
Theorem	climsubc1 15604*	Limit of a constant 𝐶 subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = ((𝐹‘𝑘) − 𝐶))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (𝐴 − 𝐶))
Theorem	climsubc2 15605*	Limit of a constant 𝐶 minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐶 − (𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (𝐶 − 𝐴))
Theorem	climle 15606*	Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	climsqz 15607*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐺‘𝑘))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)
Theorem	climsqz2 15608*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ≤ (𝐹‘𝑘))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ≤ (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)
Theorem	rlimadd 15609*	Limit of the sum of two converging functions. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ⇝𝑟 (𝐷 + 𝐸))
Theorem	rlimsub 15610*	Limit of the difference of two converging functions. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ⇝𝑟 (𝐷 − 𝐸))
Theorem	rlimmul 15611*	Limit of the product of two converging functions. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ⇝𝑟 (𝐷 · 𝐸))
Theorem	rlimdiv 15612*	Limit of the quotient of two converging functions. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸)    &   ⊢ (𝜑 → 𝐸 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) ⇝𝑟 (𝐷 / 𝐸))
Theorem	rlimneg 15613*	Limit of the negative of a sequence. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -𝐵) ⇝𝑟 -𝐶)
Theorem	rlimle 15614*	Comparison of the limits of two sequences. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → 𝐷 ≤ 𝐸)
Theorem	rlimsqzlem 15615*	Lemma for rlimsqz 15616 and rlimsqz2 15617. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥)) → (abs‘(𝐶 − 𝐸)) ≤ (abs‘(𝐵 − 𝐷)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸)
Theorem	rlimsqz 15616*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.)
⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥)) → 𝐵 ≤ 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥)) → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷)
Theorem	rlimsqz2 15617*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 3-Feb-2014.) (Revised by Mario Carneiro, 20-May-2016.)
⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥)) → 𝐶 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥)) → 𝐷 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷)
Theorem	lo1le 15618*	Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥)) → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1))
Theorem	o1le 15619*	Transfer eventual boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 25-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥)) → (abs‘𝐶) ≤ (abs‘𝐵))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1))
Theorem	rlimno1 15620*	A function whose inverse converges to zero is unbounded. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⇝𝑟 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ¬ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))
Theorem	clim2ser 15621*	The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)    ⇒   ⊢ (𝜑 → seq(𝑁 + 1)( + , 𝐹) ⇝ (𝐴 − (seq𝑀( + , 𝐹)‘𝑁)))
Theorem	clim2ser2 15622*	The limit of an infinite series with an initial segment added. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ (𝜑 → seq(𝑁 + 1)( + , 𝐹) ⇝ 𝐴)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (𝐴 + (seq𝑀( + , 𝐹)‘𝑁)))
Theorem	iserex 15623*	An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
Theorem	isermulc2 15624*	Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐶 · (𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ (𝐶 · 𝐴))
Theorem	climlec2 15625*	Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	iserle 15626*	Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)    &   ⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	iserge0 15627*	The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 0 ≤ 𝐴)
Theorem	climub 15628*	The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) ≤ 𝐴)
Theorem	climserle 15629*	The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by NM, 27-Dec-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ≤ 𝐴)
Theorem	isershft 15630	Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (seq𝑀( + , 𝐹) ⇝ 𝐴 ↔ seq(𝑀 + 𝑁)( + , (𝐹 shift 𝑁)) ⇝ 𝐴))
Theorem	isercolllem1 15631*	Lemma for isercoll 15634. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺:ℕ⟶𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)))    ⇒   ⊢ ((𝜑 ∧ 𝑆 ⊆ ℕ) → (𝐺 ↾ 𝑆) Isom < , < (𝑆, (𝐺 “ 𝑆)))
Theorem	isercolllem2 15632*	Lemma for isercoll 15634. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺:ℕ⟶𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)))    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (1...(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) = (◡𝐺 “ (𝑀...𝑁)))
Theorem	isercolllem3 15633*	Lemma for isercoll 15634. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺:ℕ⟶𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘)))    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (seq𝑀( + , 𝐹)‘𝑁) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))))
Theorem	isercoll 15634*	Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺:ℕ⟶𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ seq𝑀( + , 𝐹) ⇝ 𝐴))
Theorem	isercoll2 15635*	Generalize isercoll 15634 so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺:𝑍⟶𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑊 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝐹‘𝑛) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐻) ⇝ 𝐴 ↔ seq𝑁( + , 𝐹) ⇝ 𝐴))
Theorem	climsup 15636*	A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ sup(ran 𝐹, ℝ, < ))
Theorem	climcau 15637*	A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)
Theorem	climbdd 15638*	A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ≤ 𝑥)
Theorem	caucvgrlem 15639*	Lemma for caurcvgr 15640. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by AV, 12-Sep-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝐴 ((lim sup‘𝐹) ∈ ℝ ∧ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · 𝑅))))
Theorem	caurcvgr 15640*	A Cauchy sequence of real numbers converges to its limit supremum. The third hypothesis specifies that 𝐹 is a Cauchy sequence. (Contributed by Mario Carneiro, 7-May-2016.) (Revised by AV, 12-Sep-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ⇝𝑟 (lim sup‘𝐹))
Theorem	caucvgrlem2 15641*	Lemma for caucvgr 15642. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Mario Carneiro, 8-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))    &   ⊢ 𝐻:ℂ⟶ℝ    &   ⊢ (((𝐹‘𝑘) ∈ ℂ ∧ (𝐹‘𝑗) ∈ ℂ) → (abs‘((𝐻‘(𝐹‘𝑘)) − (𝐻‘(𝐹‘𝑗)))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))))    ⇒   ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ (𝐻‘(𝐹‘𝑛))) ⇝𝑟 ( ⇝𝑟 ‘(𝐻 ∘ 𝐹)))
Theorem	caucvgr 15642*	A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 8-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑟 )
Theorem	caurcvg 15643*	A Cauchy sequence of real numbers converges to its limit supremum. The fourth hypothesis specifies that 𝐹 is a Cauchy sequence. (Contributed by NM, 4-Apr-2005.) (Revised by AV, 12-Sep-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑚 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑚)(abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ (lim sup‘𝐹))
Theorem	caurcvg2 15644*	A Cauchy sequence of real numbers converges, existence version. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 7-Sep-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )
Theorem	caucvg 15645*	A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Proof shortened by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )
Theorem	caucvgb 15646*	A function is convergent if and only if it is Cauchy. Theorem 12-5.3 of [Gleason] p. 180. (Contributed by Mario Carneiro, 15-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)))
Theorem	serf0 15647*	If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 16-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 0)
Theorem	iseraltlem1 15648*	Lemma for iseralt 15651. A decreasing sequence with limit zero consists of positive terms. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))    &   ⊢ (𝜑 → 𝐺 ⇝ 0)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 0 ≤ (𝐺‘𝑁))
Theorem	iseraltlem2 15649*	Lemma for iseralt 15651. The terms of an alternating series form a chain of inequalities in alternate terms, so that for example 𝑆(1) ≤ 𝑆(3) ≤ 𝑆(5) ≤ ... and ... ≤ 𝑆(4) ≤ 𝑆(2) ≤ 𝑆(0) (assuming 𝑀 = 0 so that these terms are defined). (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))    &   ⊢ (𝜑 → 𝐺 ⇝ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
Theorem	iseraltlem3 15650*	Lemma for iseralt 15651. From iseraltlem2 15649, we have (-1↑𝑛) · 𝑆(𝑛 + 2𝑘) ≤ (-1↑𝑛) · 𝑆(𝑛) and (-1↑𝑛) · 𝑆(𝑛 + 1) ≤ (-1↑𝑛) · 𝑆(𝑛 + 2𝑘 + 1), and we also have (-1↑𝑛) · 𝑆(𝑛 + 1) = (-1↑𝑛) · 𝑆(𝑛) − 𝐺(𝑛 + 1) for each 𝑛 by the definition of the partial sum 𝑆, so combining the inequalities we get (-1↑𝑛) · 𝑆(𝑛) − 𝐺(𝑛 + 1) = (-1↑𝑛) · 𝑆(𝑛 + 1) ≤ (-1↑𝑛) · 𝑆(𝑛 + 2𝑘 + 1) = (-1↑𝑛) · 𝑆(𝑛 + 2𝑘) − 𝐺(𝑛 + 2𝑘 + 1) ≤ (-1↑𝑛) · 𝑆(𝑛 + 2𝑘) ≤ (-1↑𝑛) · 𝑆(𝑛) ≤ (-1↑𝑛) · 𝑆(𝑛) + 𝐺(𝑛 + 1), so ∣ (-1↑𝑛) · 𝑆(𝑛 + 2𝑘 + 1) − (-1↑𝑛) · 𝑆(𝑛) ∣ = ∣ 𝑆(𝑛 + 2𝑘 + 1) − 𝑆(𝑛) ∣ ≤ 𝐺(𝑛 + 1) and ∣ (-1↑𝑛) · 𝑆(𝑛 + 2𝑘) − (-1↑𝑛) · 𝑆(𝑛) ∣ = ∣ 𝑆(𝑛 + 2𝑘) − 𝑆(𝑛) ∣ ≤ 𝐺(𝑛 + 1). Thus, both even and odd partial sums are Cauchy if 𝐺 converges to 0. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))    &   ⊢ (𝜑 → 𝐺 ⇝ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))))
Theorem	iseralt 15651*	The alternating series test. If 𝐺(𝑘) is a decreasing sequence that converges to 0, then Σ𝑘 ∈ 𝑍(-1↑𝑘) · 𝐺(𝑘) is a convergent series. (Note that the first term is positive if 𝑀 is even, and negative if 𝑀 is odd. If the parity of your series does not match up with this, you will need to post-compose the series with multiplication by -1 using isermulc2 15624.) (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 9-Jul-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))    &   ⊢ (𝜑 → 𝐺 ⇝ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
5.10.3  Finite and infinite sums
Syntax	csu 15652	Extend class notation to include finite and infinite summations. (An underscore was added to the ASCII token in order to facilitate set.mm text searches, since "sum" is a commonly used word in comments.)
class Σ𝑘 ∈ 𝐴 𝐵
Definition	df-sum 15653*	Define the sum of a series with an index set of integers 𝐴. The variable 𝑘 is normally a free variable in 𝐵, i.e., 𝐵 can be thought of as 𝐵(𝑘). This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. These two methods of summation produce the same result on their common region of definition (i.e., finite sets of integers) by summo 15683. Examples: Σ𝑘 ∈ {1, 2, 4}𝑘 means 1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ(1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 15848). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
Theorem	sumex 15654	A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
⊢ Σ𝑘 ∈ 𝐴 𝐵 ∈ V
Theorem	sumeq1 15655	Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
Theorem	nfsum1 15656	Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ Ⅎ𝑘Σ𝑘 ∈ 𝐴 𝐵
Theorem	nfsum 15657*	Bound-variable hypothesis builder for sum: if 𝑥 is (effectively) not free in 𝐴 and 𝐵, it is not free in Σ𝑘 ∈ 𝐴𝐵. Version of nfsum 15657 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 11-Dec-2005.) (Revised by GG, 24-Feb-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥Σ𝑘 ∈ 𝐴 𝐵
Theorem	sumeq2w 15658	Equality theorem for sum, when the class expressions 𝐵 and 𝐶 are equal everywhere. Proved using only Extensionality. (Contributed by Mario Carneiro, 24-Jun-2014.) (Revised by Mario Carneiro, 13-Jun-2019.)
⊢ (∀𝑘 𝐵 = 𝐶 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	sumeq2ii 15659*	Equality theorem for sum, with the class expressions 𝐵 and 𝐶 guarded by I to be always sets. (Contributed by Mario Carneiro, 13-Jun-2019.)
⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	sumeq2 15660*	Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	cbvsum 15661*	Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ Ⅎ𝑗𝐶    ⇒   ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	cbvsumv 15662*	Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    ⇒   ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	sumeq1i 15663	Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶
Theorem	sumeq2i 15664*	Equality inference for sum. (Contributed by NM, 3-Dec-2005.)
⊢ (𝑘 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	sumeq12i 15665*	Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑘 ∈ 𝐴 → 𝐶 = 𝐷)    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷
Theorem	sumeq1d 15666	Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
Theorem	sumeq2d 15667*	Equality deduction for sum. Note that unlike sumeq2dv 15668, 𝑘 may occur in 𝜑. (Contributed by NM, 1-Nov-2005.)
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	sumeq2dv 15668*	Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	sumeq2sdv 15669*	Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.) Avoid axioms. (Revised by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	sumeq2sdvOLD 15670*	Obsolete version of sumeq2sdv 15669 as of 14-Aug-2025. (Contributed by NM, 3-Jan-2006.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)
Theorem	2sumeq2dv 15671*	Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐷)
Theorem	sumeq12dv 15672*	Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	sumeq12rdv 15673*	Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	sum2id 15674*	The second class argument to a sum can be chosen so that it is always a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 ( I ‘𝐵)
Theorem	sumfc 15675*	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 Mario Carneiro, 23-Apr-2014.)
⊢ Σ𝑗 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = Σ𝑘 ∈ 𝐴 𝐵
Theorem	fz1f1o 15676*	A lemma for working with finite sums. (Contributed by Mario Carneiro, 22-Apr-2014.)
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
Theorem	sumrblem 15677*	Lemma for sumrb 15679. (Contributed by Mario Carneiro, 12-Aug-2013.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( + , 𝐹))
Theorem	fsumcvg 15678*	The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁))
Theorem	sumrb 15679*	Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 9-Apr-2014.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑁))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹) ⇝ 𝐶 ↔ seq𝑁( + , 𝐹) ⇝ 𝐶))
Theorem	summolem3 15680*	Lemma for summo 15683. (Contributed by Mario Carneiro, 29-Mar-2014.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⦋(𝐾‘𝑛) / 𝑘⦌𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ))    &   ⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)    ⇒   ⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁))
Theorem	summolem2a 15681*	Lemma for summo 15683. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 20-Apr-2014.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⦋(𝐾‘𝑛) / 𝑘⦌𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))
Theorem	summolem2 15682*	Lemma for summo 15683. (Contributed by Mario Carneiro, 3-Apr-2014.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)    ⇒   ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
Theorem	summo 15683*	A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)    ⇒   ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))))
Theorem	zsum 15684*	Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( + , 𝐹)))
Theorem	isum 15685*	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	fsum 15686*	The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Mario Carneiro, 13-Jun-2019.)
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , 𝐺)‘𝑀))
Theorem	sum0 15687	Any sum over the empty set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
⊢ Σ𝑘 ∈ ∅ 𝐴 = 0
Theorem	sumz 15688*	Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
⊢ ((𝐴 ⊆ (ℤ≥‘𝑀) ∨ 𝐴 ∈ Fin) → Σ𝑘 ∈ 𝐴 0 = 0)
Theorem	fsumf1o 15689*	Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014.)
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)
Theorem	sumss 15690*	Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)    &   ⊢ (𝜑 → 𝐵 ⊆ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
Theorem	fsumss 15691*	Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
Theorem	sumss2 15692*	Change the index set of a sum by adding zeroes. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) ∧ (𝐵 ⊆ (ℤ≥‘𝑀) ∨ 𝐵 ∈ Fin)) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 if(𝑘 ∈ 𝐴, 𝐶, 0))
Theorem	fsumcvg2 15693*	The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.)
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁))
Theorem	fsumsers 15694*	Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 21-Apr-2014.)
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq𝑀( + , 𝐹)‘𝑁))
Theorem	fsumcvg3 15695*	A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Theorem	fsumser 15696*	A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 15713 and fsump1i 15735, which should make our notation clear and from which, along with closure fsumcl 15699, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( + , 𝐹)‘𝑁))
Theorem	fsumcl2lem 15697*	- 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 15698*	- 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 15699*	Closure of a finite sum of complex numbers 𝐴(𝑘). (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
Theorem	fsumrecl 15700*	Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)