P. 156 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15501-15600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bhmafibid2 15501	The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. Second result. (Contributed by Thierry Arnoux, 1-Feb-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
5.10  Elementary limits and convergence
5.10.1  Superior limit (lim sup)
Syntax	clsp 15502	Extend class notation to include the limsup function.
class lim sup
Definition	df-limsup 15503*	Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 15506 for its value. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 11-Sep-2020.)
⊢ lim sup = (𝑥 ∈ V ↦ inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
Theorem	limsupgord 15504	Ordering property of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → sup(((𝐹 “ (𝐵[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝐴[,)+∞)) ∩ ℝ*), ℝ*, < ))
Theorem	limsupcl 15505	Closure of the superior limit. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 12-Sep-2020.)
⊢ (𝐹 ∈ 𝑉 → (lim sup‘𝐹) ∈ ℝ*)
Theorem	limsupval 15506*	The superior limit of an infinite sequence 𝐹 of extended real numbers, which is the infimum of the set of suprema of all upper infinite subsequences of 𝐹. Definition 12-4.1 of [Gleason] p. 175. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 12-Sep-2014.)
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    ⇒   ⊢ (𝐹 ∈ 𝑉 → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, < ))
Theorem	limsupgf 15507*	Closure of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    ⇒   ⊢ 𝐺:ℝ⟶ℝ*
Theorem	limsupgval 15508*	Value of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    ⇒   ⊢ (𝑀 ∈ ℝ → (𝐺‘𝑀) = sup(((𝐹 “ (𝑀[,)+∞)) ∩ ℝ*), ℝ*, < ))
Theorem	limsupgle 15509*	The defining property of the superior limit function. (Contributed by Mario Carneiro, 5-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    ⇒   ⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝐺‘𝐶) ≤ 𝐴 ↔ ∀𝑗 ∈ 𝐵 (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴)))
Theorem	limsuple 15510*	The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    ⇒   ⊢ ((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐴 ≤ (lim sup‘𝐹) ↔ ∀𝑗 ∈ ℝ 𝐴 ≤ (𝐺‘𝑗)))
Theorem	limsuplt 15511*	The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    ⇒   ⊢ ((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ* ∧ 𝐴 ∈ ℝ*) → ((lim sup‘𝐹) < 𝐴 ↔ ∃𝑗 ∈ ℝ (𝐺‘𝑗) < 𝐴))
Theorem	limsupval2 15512*	The superior limit, relativized to an unbounded set. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) = inf((𝐺 “ 𝐴), ℝ*, < ))
Theorem	limsupgre 15513*	If a sequence of real numbers has upper bounded limit supremum, then all the partial suprema are real. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) → 𝐺:ℝ⟶ℝ)
Theorem	limsupbnd1 15514*	If a sequence is eventually at most 𝐴, then the limsup is also at most 𝐴. (The converse is only true if the less or equal is replaced by strictly less than; consider the sequence 1 / 𝑛 which is never less or equal to zero even though the limsup is.) (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐵⟶ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) ≤ 𝐴)
Theorem	limsupbnd2 15515*	If a sequence is eventually greater than 𝐴, then the limsup is also greater than 𝐴. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐵⟶ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → sup(𝐵, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)))    ⇒   ⊢ (𝜑 → 𝐴 ≤ (lim sup‘𝐹))
5.10.2  Limits
Syntax	cli 15516	Extend class notation with convergence relation for limits.
class ⇝
Syntax	crli 15517	Extend class notation with real convergence relation for limits.
class ⇝𝑟
Syntax	co1 15518	Extend class notation with the set of all eventually bounded functions.
class 𝑂(1)
Syntax	clo1 15519	Extend class notation with the set of all eventually upper bounded functions.
class ≤𝑂(1)
Definition	df-clim 15520*	Define the limit relation for complex number sequences. See clim 15526 for its relational expression. (Contributed by NM, 28-Aug-2005.)
⊢ ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}
Definition	df-rlim 15521*	Define the limit relation for partial functions on the reals. See rlim 15527 for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ ⇝𝑟 = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))}
Definition	df-o1 15522*	Define the set of eventually bounded functions. We don't bother to build the full conception of big-O notation, because we can represent any big-O in terms of 𝑂(1) and division, and any little-O in terms of a limit and division. We could also use limsup for this, but it only works on integer sequences, while this will work for real sequences or integer sequences. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ 𝑂(1) = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}
Definition	df-lo1 15523*	Define the set of eventually upper bounded real functions. This fills a gap in 𝑂(1) coverage, to express statements like 𝑓(𝑥) ≤ 𝑔(𝑥) + 𝑂(𝑥) via (𝑥 ∈ ℝ+ ↦ (𝑓(𝑥) − 𝑔(𝑥)) / 𝑥) ∈ ≤𝑂(1). (Contributed by Mario Carneiro, 25-May-2016.)
⊢ ≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚}
Theorem	climrel 15524	The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ Rel ⇝
Theorem	rlimrel 15525	The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014.)
⊢ Rel ⇝𝑟
Theorem	clim 15526*	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	rlim 15527*	Express the predicate: The limit of complex number function 𝐹 is 𝐶, or 𝐹 converges to 𝐶, in the real sense. This means that for any real 𝑥, no matter how small, there always exists a number 𝑦 such that the absolute difference of any number in the function beyond 𝑦 and the limit is less than 𝑥. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝𝑟 𝐶 ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))))
Theorem	rlim2 15528*	Rewrite rlim 15527 for a mapping operation. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.)
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥)))
Theorem	rlim2lt 15529*	Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥)))
Theorem	rlim3 15530*	Restrict the range of the domain bound to reals greater than some 𝐷 ∈ ℝ. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥)))
Theorem	climcl 15531	Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ)
Theorem	rlimpm 15532	Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ (ℂ ↑pm ℝ))
Theorem	rlimf 15533	Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝐹 ⇝𝑟 𝐴 → 𝐹:dom 𝐹⟶ℂ)
Theorem	rlimss 15534	Domain closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝐹 ⇝𝑟 𝐴 → dom 𝐹 ⊆ ℝ)
Theorem	rlimcl 15535	Closure of the limit of a sequence of complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐹 ⇝𝑟 𝐴 → 𝐴 ∈ ℂ)
Theorem	clim2 15536*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 15526. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	clim2c 15537*	Express the predicate 𝐹 converges to 𝐴. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝑥))
Theorem	clim0 15538*	Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘𝐵) < 𝑥)))
Theorem	clim0c 15539*	Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝑥))
Theorem	rlim0 15540*	Express the predicate 𝐵(𝑧) converges to 0. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.)
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘𝐵) < 𝑥)))
Theorem	rlim0lt 15541*	Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.)
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘𝐵) < 𝑥)))
Theorem	climi 15542*	Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝐶))
Theorem	climi2 15543*	Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝐶)
Theorem	climi0 15544*	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	rlimi 15545*	Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 28-Feb-2015.)
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑅))
Theorem	rlimi2 15546*	Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑅))
Theorem	ello1 15547*	Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝐹 ∈ ≤𝑂(1) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚))
Theorem	ello12 15548*	Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ ≤𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚)))
Theorem	ello12r 15549*	Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝑥 → (𝐹‘𝑥) ≤ 𝑀)) → 𝐹 ∈ ≤𝑂(1))
Theorem	lo1f 15550	An eventually upper bounded function is a function. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝐹 ∈ ≤𝑂(1) → 𝐹:dom 𝐹⟶ℝ)
Theorem	lo1dm 15551	An eventually upper bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝐹 ∈ ≤𝑂(1) → dom 𝐹 ⊆ ℝ)
Theorem	lo1bdd 15552*	The defining property of an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝐹 ∈ ≤𝑂(1) ∧ 𝐹:𝐴⟶ℝ) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚))
Theorem	ello1mpt 15553*	Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔ ∃𝑦 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚)))
Theorem	ello1mpt2 15554*	Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔ ∃𝑦 ∈ (𝐶[,)+∞)∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚)))
Theorem	ello1d 15555*	Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥)) → 𝐵 ≤ 𝑀)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))
Theorem	lo1bdd2 15556*	If an eventually bounded function is bounded on every interval 𝐴 ∩ (-∞, 𝑦) by a function 𝑀(𝑦), then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝐵 ≤ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚)
Theorem	lo1bddrp 15557*	Refine o1bdd2 15573 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝐵 ≤ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℝ+ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚)
Theorem	elo1 15558*	Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐹 ∈ 𝑂(1) ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚))
Theorem	elo12 15559*	Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ 𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚)))
Theorem	elo12r 15560*	Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑀)) → 𝐹 ∈ 𝑂(1))
Theorem	o1f 15561	An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)
Theorem	o1dm 15562	An eventually bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ)
Theorem	o1bdd 15563*	The defining property of an eventually bounded function. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:𝐴⟶ℂ) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚))
Theorem	lo1o1 15564	A function is eventually bounded iff its absolute value is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ∈ 𝑂(1) ↔ (abs ∘ 𝐹) ∈ ≤𝑂(1)))
Theorem	lo1o12 15565*	A function is eventually bounded iff its absolute value is eventually upper bounded. (This function is useful for converting theorems about ≤𝑂(1) to 𝑂(1).) (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1) ↔ (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ ≤𝑂(1)))
Theorem	elo1mpt 15566*	Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 21-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1) ↔ ∃𝑦 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑚)))
Theorem	elo1mpt2 15567*	Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 12-May-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1) ↔ ∃𝑦 ∈ (𝐶[,)+∞)∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑚)))
Theorem	elo1d 15568*	Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 21-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥)) → (abs‘𝐵) ≤ 𝑀)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))
Theorem	o1lo1 15569*	A real function is eventually bounded iff it is eventually lower bounded and eventually upper bounded. (Contributed by Mario Carneiro, 25-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ∧ (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ ≤𝑂(1))))
Theorem	o1lo12 15570*	A lower bounded real function is eventually bounded iff it is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1) ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)))
Theorem	o1lo1d 15571*	A real eventually bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))
Theorem	icco1 15572*	Derive eventual boundedness from separate upper and lower eventual bounds. (Contributed by Mario Carneiro, 15-Apr-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥)) → 𝐵 ∈ (𝑀[,]𝑁))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))
Theorem	o1bdd2 15573*	If an eventually bounded function is bounded on every interval 𝐴 ∩ (-∞, 𝑦) by a function 𝑀(𝑦), then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘𝐵) ≤ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑚)
Theorem	o1bddrp 15574*	Refine o1bdd2 15573 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘𝐵) ≤ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑚)
Theorem	climconst 15575*	An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
Theorem	rlimconst 15576*	A constant sequence converges to its value. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐵)
Theorem	rlimclim1 15577	Forward direction of rlimclim 15578. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐴)    &   ⊢ (𝜑 → 𝑍 ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
Theorem	rlimclim 15578	A sequence on an upper integer set converges in the real sense iff it converges in the integer sense. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝𝑟 𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	climrlim2 15579*	Produce a real limit from an integer limit, where the real function is only dependent on the integer part of 𝑥. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝑛 = (⌊‘𝑥) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ≤ 𝑥)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷)
Theorem	climconst2 15580	A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ (ℤ≥‘𝑀) ⊆ 𝑍    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝐴}) ⇝ 𝐴)
Theorem	climz 15581	The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ (ℤ × {0}) ⇝ 0
Theorem	rlimuni 15582	A real function whose domain is unbounded above converges to at most one limit. (Contributed by Mario Carneiro, 8-May-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐵)    &   ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	rlimdm 15583	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, 8-May-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 ‘𝐹)))
Theorem	climuni 15584	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 15585	The limit relation is function-like, and with codomain the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ ⇝ :dom ⇝ ⟶ℂ
Theorem	climdm 15586	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 15587*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 𝐹 ⇝ 𝑥)
Theorem	climreu 15588*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 ∈ ℂ 𝐹 ⇝ 𝑥)
Theorem	climmo 15589*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)
⊢ ∃*𝑥 𝐹 ⇝ 𝑥
Theorem	rlimres 15590	The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝐹 ⇝𝑟 𝐴 → (𝐹 ↾ 𝐵) ⇝𝑟 𝐴)
Theorem	lo1res 15591	The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐹 ∈ ≤𝑂(1) → (𝐹 ↾ 𝐴) ∈ ≤𝑂(1))
Theorem	o1res 15592	The restriction of an eventually bounded function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ (𝐹 ∈ 𝑂(1) → (𝐹 ↾ 𝐴) ∈ 𝑂(1))
Theorem	rlimres2 15593*	The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ⇝𝑟 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷)
Theorem	lo1res2 15594*	The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ ≤𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1))
Theorem	o1res2 15595*	The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1))
Theorem	lo1resb 15596	The restriction of a function to an unbounded-above interval is eventually upper bounded iff the original is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ ≤𝑂(1) ↔ (𝐹 ↾ (𝐵[,)+∞)) ∈ ≤𝑂(1)))
Theorem	rlimresb 15597	The restriction of a function to an unbounded-above interval converges iff the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝𝑟 𝐶 ↔ (𝐹 ↾ (𝐵[,)+∞)) ⇝𝑟 𝐶))
Theorem	o1resb 15598	The restriction of a function to an unbounded-above interval is eventually bounded iff the original is eventually bounded. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑂(1) ↔ (𝐹 ↾ (𝐵[,)+∞)) ∈ 𝑂(1)))
Theorem	climeq 15599*	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	lo1eq 15600*	Two functions that are eventually equal to one another are eventually bounded if one of them is. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥)) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1)))