P. 158 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15701-15800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	climdm 15701	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 15702*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 𝐹 ⇝ 𝑥)
Theorem	climreu 15703*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 ∈ ℂ 𝐹 ⇝ 𝑥)
Theorem	climmo 15704*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)
⊢ ∃*𝑥 𝐹 ⇝ 𝑥
Theorem	rlimres 15705	The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝐹 ⇝𝑟 𝐴 → (𝐹 ↾ 𝐵) ⇝𝑟 𝐴)
Theorem	lo1res 15706	The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐹 ∈ ≤𝑂(1) → (𝐹 ↾ 𝐴) ∈ ≤𝑂(1))
Theorem	o1res 15707	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 15708*	The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ⇝𝑟 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷)
Theorem	lo1res2 15709*	The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ ≤𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1))
Theorem	o1res2 15710*	The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1))
Theorem	lo1resb 15711	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 15712	The restriction of a function to an unbounded-above interval converges iff the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝𝑟 𝐶 ↔ (𝐹 ↾ (𝐵[,)+∞)) ⇝𝑟 𝐶))
Theorem	o1resb 15713	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 15714*	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 15715*	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)))
Theorem	rlimeq 15716*	Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥)) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐸 ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸))
Theorem	o1eq 15717*	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)))
Theorem	climmpt 15718*	Exhibit a function 𝐺 with the same convergence properties as the not-quite-function 𝐹. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	2clim 15719*	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	climmpt2 15720*	Relate an integer limit on a not-quite-function to a real limit. (Contributed by Mario Carneiro, 17-Sep-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝑛 ∈ 𝑍 ↦ (𝐹‘𝑛)) ⇝𝑟 𝐴))
Theorem	climshftlem 15721	A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝑀 ∈ ℤ → (𝐹 ⇝ 𝐴 → (𝐹 shift 𝑀) ⇝ 𝐴))
Theorem	climres 15722	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 15723	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 15724	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	rlimcld2 15725*	If 𝐷 is a closed set in the topology of the complex numbers (stated here in basic form), and all the elements of the sequence lie in 𝐷, then the limit of the sequence also lies in 𝐷. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    &   ⊢ (𝜑 → 𝐷 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ 𝐷)) → 𝑅 ∈ ℝ+)    &   ⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ 𝐷)) ∧ 𝑧 ∈ 𝐷) → 𝑅 ≤ (abs‘(𝑧 − 𝑦)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	rlimrege0 15726*	The limit of a sequence of complex numbers with nonnegative real part has nonnegative real part. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (ℜ‘𝐵))    ⇒   ⊢ (𝜑 → 0 ≤ (ℜ‘𝐶))
Theorem	rlimrecl 15727*	The limit of a real sequence is real. (Contributed by Mario Carneiro, 9-May-2016.)
⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ℝ)
Theorem	rlimge0 15728*	The limit of a sequence of nonnegative reals is nonnegative. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ 𝐶)
Theorem	climshft2 15729*	A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 𝐾)) = (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	climrecl 15730*	The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.) (Proof shortened by Mario Carneiro, 10-May-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	climge0 15731*	A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.) (Proof shortened by Mario Carneiro, 10-May-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 0 ≤ 𝐴)
Theorem	climabs0 15732*	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	o1co 15733*	Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑂(1))    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ 𝑂(1))
Theorem	o1compt 15734*	Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑂(1))    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ 𝐶))    ⇒   ⊢ (𝜑 → (𝐹 ∘ (𝑦 ∈ 𝐵 ↦ 𝐶)) ∈ 𝑂(1))
Theorem	rlimcn1 15735*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014.)
⊢ (𝜑 → 𝐺:𝐴⟶𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝𝑟 𝐶)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝𝑟 (𝐹‘𝐶))
Theorem	rlimcn1b 15736*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)) ⇝𝑟 (𝐹‘𝐶))
Theorem	rlimcn3 15737*	Image of a limit under a continuous map, two-arg version. Originally a subproof of rlimcn2 15738. (Contributed by SN, 27-Sep-2024.)
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐵𝐹𝐶) ∈ ℂ)    &   ⊢ (𝜑 → (𝑅𝐹𝑆) ∈ ℂ)    &   ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝑅)    &   ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥))    ⇒   ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ (𝐵𝐹𝐶)) ⇝𝑟 (𝑅𝐹𝑆))
Theorem	rlimcn2 15738*	Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014.)
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝑅)    &   ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝑆)    &   ⊢ (𝜑 → 𝐹:(𝑋 × 𝑌)⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥))    ⇒   ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ (𝐵𝐹𝐶)) ⇝𝑟 (𝑅𝐹𝑆))
Theorem	climcn1 15739*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐵 ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) < 𝑥))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐹‘𝐴))
Theorem	climcn2 15740*	Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐶 ∧ 𝑣 ∈ 𝐷)) → (𝑢𝐹𝑣) ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ⇝ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐾‘𝑘) = ((𝐺‘𝑘)𝐹(𝐻‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐾 ⇝ (𝐴𝐹𝐵))
Theorem	addcn2 15741*	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 23525 and df-cncf 25179 are not yet available to us. See addcn 25165 for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))
Theorem	subcn2 15742*	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 15743*	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	reccn2 15744*	The reciprocal function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) (Revised by Mario Carneiro, 22-Sep-2014.)
⊢ 𝑇 = (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2))    ⇒   ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))
Theorem	cn1lem 15745*	A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ 𝐹:ℂ⟶ℂ    &   ⊢ ((𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) ≤ (abs‘(𝑧 − 𝐴)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) < 𝑥))
Theorem	abscn2 15746*	The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((abs‘𝑧) − (abs‘𝐴))) < 𝑥))
Theorem	cjcn2 15747*	The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((∗‘𝑧) − (∗‘𝐴))) < 𝑥))
Theorem	recn2 15748*	The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((ℜ‘𝑧) − (ℜ‘𝐴))) < 𝑥))
Theorem	imcn2 15749*	The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((ℑ‘𝑧) − (ℑ‘𝐴))) < 𝑥))
Theorem	climcn1lem 15750*	The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ 𝐻:ℂ⟶ℂ    &   ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐻‘𝑧) − (𝐻‘𝐴))) < 𝑥))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐻‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (𝐻‘𝐴))
Theorem	climabs 15751*	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 15752*	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 15753*	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 15754*	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	rlimmptrcl 15755*	Reverse closure for a real limit. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
Theorem	rlimabs 15756*	Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (abs‘𝐵)) ⇝𝑟 (abs‘𝐶))
Theorem	rlimcj 15757*	Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (∗‘𝐵)) ⇝𝑟 (∗‘𝐶))
Theorem	rlimre 15758*	Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (ℜ‘𝐵)) ⇝𝑟 (ℜ‘𝐶))
Theorem	rlimim 15759*	Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (ℑ‘𝐵)) ⇝𝑟 (ℑ‘𝐶))
Theorem	o1of2 15760*	Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈ ℝ)    &   ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝑅𝑦) ∈ ℂ)    &   ⊢ (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))    ⇒   ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))
Theorem	o1add 15761	The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (𝐹 ∘f + 𝐺) ∈ 𝑂(1))
Theorem	o1mul 15762	The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (𝐹 ∘f · 𝐺) ∈ 𝑂(1))
Theorem	o1sub 15763	The difference of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (𝐹 ∘f − 𝐺) ∈ 𝑂(1))
Theorem	rlimo1 15764	Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ (𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ 𝑂(1))
Theorem	rlimdmo1 15765	A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ (𝐹 ∈ dom ⇝𝑟 → 𝐹 ∈ 𝑂(1))
Theorem	o1rlimmul 15766	The product of an eventually bounded function and a function of limit zero has limit zero. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0) → (𝐹 ∘f · 𝐺) ⇝𝑟 0)
Theorem	o1const 15767*	A constant function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))
Theorem	lo1const 15768*	A constant function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))
Theorem	lo1mptrcl 15769*	Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
Theorem	o1mptrcl 15770*	Reverse closure for an eventually bounded function. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
Theorem	o1add2 15771*	The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝑂(1))
Theorem	o1mul2 15772*	The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∈ 𝑂(1))
Theorem	o1sub2 15773*	The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ 𝑂(1))
Theorem	lo1add 15774*	The sum of two eventually upper bounded functions is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ ≤𝑂(1))
Theorem	lo1mul 15775*	The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∈ ≤𝑂(1))
Theorem	lo1mul2 15776*	The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ ≤𝑂(1))
Theorem	o1dif 15777*	If the difference of two functions is eventually bounded, eventual boundedness of either one implies the other. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1) ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1)))
Theorem	lo1sub 15778*	The difference of an eventually upper bounded function and an eventually bounded function is eventually upper bounded. The "correct" sharp result here takes the second function to be eventually lower bounded instead of just bounded, but our notation for this is simply (𝑥 ∈ 𝐴 ↦ -𝐶) ∈ ≤𝑂(1), so it is just a special case of lo1add 15774. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ ≤𝑂(1))
Theorem	climadd 15779*	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 15780*	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 15781*	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 15782*	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 15783*	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 15784*	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 15785*	Limit of a constant 𝐶 subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = ((𝐹‘𝑘) − 𝐶))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ (𝐴 − 𝐶))
Theorem	climsubc2 15786*	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 15787*	Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	climsqz 15788*	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 15789*	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 15790*	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 15791*	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 15792*	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 15793*	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 15794*	Limit of the negative of a sequence. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -𝐵) ⇝𝑟 -𝐶)
Theorem	rlimle 15795*	Comparison of the limits of two sequences. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → 𝐷 ≤ 𝐸)
Theorem	rlimsqzlem 15796*	Lemma for rlimsqz 15797 and rlimsqz2 15798. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥)) → (abs‘(𝐶 − 𝐸)) ≤ (abs‘(𝐵 − 𝐷)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸)
Theorem	rlimsqz 15797*	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 15798*	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 15799*	Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥)) → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1))
Theorem	o1le 15800*	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))