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	xrmaxcl 12001	The maximum of two extended reals is an extended real. (Contributed by Jim Kingdon, 29-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → sup({𝐴, 𝐵}, ℝ*, < ) ∈ ℝ*)
Theorem	xrmax1sup 12002	An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ*, < ))
Theorem	xrmax2sup 12003	An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐵 ≤ sup({𝐴, 𝐵}, ℝ*, < ))
Theorem	xrmaxrecl 12004	The maximum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 30-Apr-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ*, < ) = sup({𝐴, 𝐵}, ℝ, < ))
Theorem	xrmaxleastlt 12005	The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 < sup({𝐴, 𝐵}, ℝ*, < ))) → (𝐶 < 𝐴 ∨ 𝐶 < 𝐵))
Theorem	xrltmaxsup 12006	The maximum as a least upper bound. (Contributed by Jim Kingdon, 10-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 < sup({𝐴, 𝐵}, ℝ*, < ) ↔ (𝐶 < 𝐴 ∨ 𝐶 < 𝐵)))
Theorem	xrmaxltsup 12007	Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 30-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)))
Theorem	xrmaxlesup 12008	Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 10-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (sup({𝐴, 𝐵}, ℝ*, < ) ≤ 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶)))
Theorem	xrmaxaddlem 12009	Lemma for xrmaxadd 12010. The case where 𝐴 is real. (Contributed by Jim Kingdon, 11-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
Theorem	xrmaxadd 12010	Distributing addition over maximum. (Contributed by Jim Kingdon, 11-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
4.8.8  The minimum of two extended reals
Theorem	xrnegiso 12011	Negation is an order anti-isomorphism of the extended reals, which is its own inverse. (Contributed by Jim Kingdon, 2-May-2023.)
⊢ 𝐹 = (𝑥 ∈ ℝ* ↦ -𝑒𝑥)    ⇒   ⊢ (𝐹 Isom < , ◡ < (ℝ*, ℝ*) ∧ ◡𝐹 = 𝐹)
Theorem	infxrnegsupex 12012*	The infimum of a set of extended reals 𝐴 is the negative of the supremum of the negatives of its elements. (Contributed by Jim Kingdon, 2-May-2023.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ*)    ⇒   ⊢ (𝜑 → inf(𝐴, ℝ*, < ) = -𝑒sup({𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ 𝐴}, ℝ*, < ))
Theorem	xrnegcon1d 12013	Contraposition law for extended real unary minus. (Contributed by Jim Kingdon, 2-May-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (-𝑒𝐴 = 𝐵 ↔ -𝑒𝐵 = 𝐴))
Theorem	xrminmax 12014	Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 2-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → inf({𝐴, 𝐵}, ℝ*, < ) = -𝑒sup({-𝑒𝐴, -𝑒𝐵}, ℝ*, < ))
Theorem	xrmincl 12015	The minumum of two extended reals is an extended real. (Contributed by Jim Kingdon, 3-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → inf({𝐴, 𝐵}, ℝ*, < ) ∈ ℝ*)
Theorem	xrmin1inf 12016	The minimum of two extended reals is less than or equal to the first. (Contributed by Jim Kingdon, 3-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → inf({𝐴, 𝐵}, ℝ*, < ) ≤ 𝐴)
Theorem	xrmin2inf 12017	The minimum of two extended reals is less than or equal to the second. (Contributed by Jim Kingdon, 3-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → inf({𝐴, 𝐵}, ℝ*, < ) ≤ 𝐵)
Theorem	xrmineqinf 12018	The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) (Revised by Jim Kingdon, 3-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐴) → inf({𝐴, 𝐵}, ℝ*, < ) = 𝐵)
Theorem	xrltmininf 12019	Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 3-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 < inf({𝐵, 𝐶}, ℝ*, < ) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶)))
Theorem	xrlemininf 12020	Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 4-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ≤ inf({𝐵, 𝐶}, ℝ*, < ) ↔ (𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶)))
Theorem	xrminltinf 12021	Two ways of saying an extended real is greater than the minimum of two others. (Contributed by Jim Kingdon, 19-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (inf({𝐵, 𝐶}, ℝ*, < ) < 𝐴 ↔ (𝐵 < 𝐴 ∨ 𝐶 < 𝐴)))
Theorem	xrminrecl 12022	The minimum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 18-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ*, < ) = inf({𝐴, 𝐵}, ℝ, < ))
Theorem	xrminrpcl 12023	The minimum of two positive reals is a positive real. (Contributed by Jim Kingdon, 4-May-2023.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → inf({𝐴, 𝐵}, ℝ*, < ) ∈ ℝ+)
Theorem	xrminadd 12024	Distributing addition over minimum. (Contributed by Jim Kingdon, 10-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → inf({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 inf({𝐵, 𝐶}, ℝ*, < )))
Theorem	xrbdtri 12025	Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 < 𝐶)) → inf({(𝐴 +𝑒 𝐵), 𝐶}, ℝ*, < ) ≤ (inf({𝐴, 𝐶}, ℝ*, < ) +𝑒 inf({𝐵, 𝐶}, ℝ*, < )))
Theorem	iooinsup 12026	Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 22-May-2023.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = (sup({𝐴, 𝐶}, ℝ*, < )(,)inf({𝐵, 𝐷}, ℝ*, < )))
4.9  Elementary limits and convergence
4.9.1  Limits
Syntax	cli 12027	Extend class notation with convergence relation for limits.
class ⇝
Definition	df-clim 12028*	Define the limit relation for complex number sequences. See clim 12030 for its relational expression. (Contributed by NM, 28-Aug-2005.)
⊢ ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}
Theorem	climrel 12029	The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ Rel ⇝
Theorem	clim 12030*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. This means that for any real 𝑥, no matter how small, there always exists an integer 𝑗 such that the absolute difference of any later complex number in the sequence and the limit is less than 𝑥. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	climcl 12031	Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ)
Theorem	clim2 12032*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 12030. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	clim2c 12033*	Express the predicate 𝐹 converges to 𝐴. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝑥))
Theorem	clim0 12034*	Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘𝐵) < 𝑥)))
Theorem	clim0c 12035*	Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝑥))
Theorem	climi 12036*	Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝐶))
Theorem	climi2 12037*	Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝐶)
Theorem	climi0 12038*	Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐹 ⇝ 0)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝐶)
Theorem	climconst 12039*	An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
Theorem	climconst2 12040	A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ (ℤ≥‘𝑀) ⊆ 𝑍    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝐴}) ⇝ 𝐴)
Theorem	climz 12041	The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ (ℤ × {0}) ⇝ 0
Theorem	climuni 12042	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵) → 𝐴 = 𝐵)
Theorem	fclim 12043	The limit relation is function-like, and with codomian the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ ⇝ :dom ⇝ ⟶ℂ
Theorem	climdm 12044	Two ways to express that a function has a limit. (The expression ( ⇝ ‘𝐹) is sometimes useful as a shorthand for "the unique limit of the function 𝐹"). (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ (𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘𝐹))
Theorem	climeu 12045*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 𝐹 ⇝ 𝑥)
Theorem	climreu 12046*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 ∈ ℂ 𝐹 ⇝ 𝑥)
Theorem	climmo 12047*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)
⊢ ∃*𝑥 𝐹 ⇝ 𝑥
Theorem	climeq 12048*	Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	climmpt 12049*	Exhibit a function 𝐺 with the same convergence properties as the not-quite-function 𝐹. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	2clim 12050*	If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑥)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)
Theorem	climshftlemg 12051	A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ 𝐴 → (𝐹 shift 𝑀) ⇝ 𝐴))
Theorem	climres 12052	A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → ((𝐹 ↾ (ℤ≥‘𝑀)) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	climshft 12053	A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → ((𝐹 shift 𝑀) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	serclim0 12054	The zero series converges to zero. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
⊢ (𝑀 ∈ ℤ → seq𝑀( + , ((ℤ≥‘𝑀) × {0})) ⇝ 0)
Theorem	climshft2 12055*	A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 𝐾)) = (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	climabs0 12056*	Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ 𝐺 ⇝ 0))
Theorem	climcn1 12057*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐵 ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) < 𝑥))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐹‘𝐴))
Theorem	climcn2 12058*	Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐶 ∧ 𝑣 ∈ 𝐷)) → (𝑢𝐹𝑣) ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ⇝ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐾‘𝑘) = ((𝐺‘𝑘)𝐹(𝐻‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐾 ⇝ (𝐴𝐹𝐵))
Theorem	addcn2 12059*	Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (We write out the definition directly because df-cn and df-cncf are not yet available to us. See addcncntop 15646 for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))
Theorem	subcn2 12060*	Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶))) < 𝐴))
Theorem	mulcn2 12061*	Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴))
Theorem	reccn2ap 12062*	The reciprocal function is continuous. The class 𝑇 is just for convenience in writing the proof and typically would be passed in as an instance of eqid 2238. (Contributed by Mario Carneiro, 9-Feb-2014.) Using apart, infimum of pair. (Revised by Jim Kingdon, 26-May-2023.)
⊢ 𝑇 = (inf({1, ((abs‘𝐴) · 𝐵)}, ℝ, < ) · ((abs‘𝐴) / 2))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝐵 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 0} ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))
Theorem	cn1lem 12063*	A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ 𝐹:ℂ⟶ℂ    &   ⊢ ((𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) ≤ (abs‘(𝑧 − 𝐴)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) < 𝑥))
Theorem	abscn2 12064*	The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((abs‘𝑧) − (abs‘𝐴))) < 𝑥))
Theorem	cjcn2 12065*	The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((∗‘𝑧) − (∗‘𝐴))) < 𝑥))
Theorem	recn2 12066*	The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((ℜ‘𝑧) − (ℜ‘𝐴))) < 𝑥))
Theorem	imcn2 12067*	The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((ℑ‘𝑧) − (ℑ‘𝐴))) < 𝑥))
Theorem	climcn1lem 12068*	The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ 𝐻:ℂ⟶ℂ    &   ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐻‘𝑧) − (𝐻‘𝐴))) < 𝑥))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐻‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (𝐻‘𝐴))
Theorem	climabs 12069*	Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (abs‘𝐴))
Theorem	climcj 12070*	Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (∗‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (∗‘𝐴))
Theorem	climre 12071*	Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (ℜ‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (ℜ‘𝐴))
Theorem	climim 12072*	Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (ℑ‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (ℑ‘𝐴))
Theorem	climrecl 12073*	The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	climge0 12074*	A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 0 ≤ 𝐴)
Theorem	climadd 12075*	Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by NM, 24-Sep-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 + 𝐵))
Theorem	climmul 12076*	Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by NM, 27-Dec-2005.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 · 𝐵))
Theorem	climsub 12077*	Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 − 𝐵))
Theorem	climaddc1 12078*	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 12079*	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 12080*	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 12081*	Limit of a constant 𝐶 subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = ((𝐹‘𝑘) − 𝐶))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (𝐴 − 𝐶))
Theorem	climsubc2 12082*	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 12083*	Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	climsqz 12084*	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 12085*	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	clim2ser 12086*	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 12087*	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 12088*	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 12089*	Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐶 · (𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ (𝐶 · 𝐴))
Theorem	climlec2 12090*	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 12091*	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 12092*	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 12093*	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 12094*	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	iser3shft 12095*	Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Jim Kingdon, 17-Oct-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹) ⇝ 𝐴 ↔ seq(𝑀 + 𝑁)( + , (𝐹 shift 𝑁)) ⇝ 𝐴))
Theorem	climcau 12096*	A converging sequence of complex numbers is a Cauchy sequence. The converse would require excluded middle or a different definition of Cauchy sequence (for example, fixing a rate of convergence as in climcvg1n 12099). 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	climrecvg1n 12097*	A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within 𝐶 / 𝑛 of the nth term, where 𝐶 is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )
Theorem	climcvg1nlem 12098*	Lemma for climcvg1n 12099. We construct sequences of the real and imaginary parts of each term of 𝐹, show those converge, and use that to show that 𝐹 converges. (Contributed by Jim Kingdon, 24-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛))    &   ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ (ℜ‘(𝐹‘𝑥)))    &   ⊢ 𝐻 = (𝑥 ∈ ℕ ↦ (ℑ‘(𝐹‘𝑥)))    &   ⊢ 𝐽 = (𝑥 ∈ ℕ ↦ (i · (𝐻‘𝑥)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )
Theorem	climcvg1n 12099*	A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within 𝐶 / 𝑛 of the nth term, where 𝐶 is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )
Theorem	climcaucn 12100*	A converging sequence of complex numbers is a Cauchy sequence. This is like climcau 12096 but adds the part that (𝐹‘𝑘) is complex. (Contributed by Jim Kingdon, 24-Aug-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))