Home | Metamath
Proof Explorer Theorem List (p. 149 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | releabsd 14801 | The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘𝐴) ≤ (abs‘𝐴)) | ||
Theorem | absexpd 14802 | Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) | ||
Theorem | abssubd 14803 | Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐵 − 𝐴))) | ||
Theorem | absmuld 14804 | Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵))) | ||
Theorem | absdivd 14805 | Absolute value distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) | ||
Theorem | abstrid 14806 | Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 + 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))) | ||
Theorem | abs2difd 14807 | Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))) | ||
Theorem | abs2dif2d 14808 | Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))) | ||
Theorem | abs2difabsd 14809 | Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵))) | ||
Theorem | abs3difd 14810 | Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵)))) | ||
Theorem | abs3lemd 14811 | Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) < (𝐷 / 2)) & ⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < 𝐷) | ||
Theorem | reusq0 14812* | A complex number is the square of exactly one complex number iff the given complex number is zero. (Contributed by AV, 21-Jun-2023.) |
⊢ (𝑋 ∈ ℂ → (∃!𝑥 ∈ ℂ (𝑥↑2) = 𝑋 ↔ 𝑋 = 0)) | ||
Theorem | bhmafibid1cn 14813 | The Brahmagupta-Fibonacci identity for complex numbers. Express the product of two sums of two squares as a sum of two squares. First result. (Contributed by Thierry Arnoux, 1-Feb-2020.) Generalization for complex numbers proposed by GL. (Revised by AV, 8-Jun-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) | ||
Theorem | bhmafibid2cn 14814 | The Brahmagupta-Fibonacci identity for complex numbers. Express the product of two sums of two squares as a sum of two squares. Second result. (Contributed by Thierry Arnoux, 1-Feb-2020.) Generalization for complex numbers proposed by GL. (Revised by AV, 8-Jun-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))) | ||
Theorem | bhmafibid1 14815 | The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. First result. Remark: The proof uses a different approach than the proof of bhmafibid1cn 14813, and is a little bit shorter. (Contributed by Thierry Arnoux, 1-Feb-2020.) (Proof modification is discouraged.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) | ||
Theorem | bhmafibid2 14816 | 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))) | ||
Syntax | clsp 14817 | Extend class notation to include the limsup function. |
class lim sup | ||
Definition | df-limsup 14818* | Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 14821 for its value. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 11-Sep-2020.) |
⊢ lim sup = (𝑥 ∈ V ↦ inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < )) | ||
Theorem | limsupgord 14819 | 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 14820 | Closure of the superior limit. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 12-Sep-2020.) |
⊢ (𝐹 ∈ 𝑉 → (lim sup‘𝐹) ∈ ℝ*) | ||
Theorem | limsupval 14821* | 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 14822* | Closure of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ 𝐺:ℝ⟶ℝ* | ||
Theorem | limsupgval 14823* | Value of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ (𝑀 ∈ ℝ → (𝐺‘𝑀) = sup(((𝐹 “ (𝑀[,)+∞)) ∩ ℝ*), ℝ*, < )) | ||
Theorem | limsupgle 14824* | 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 14825* | 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 14826* | 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 14827* | 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 14828* | 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 14829* | 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 14830* | 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‘𝐹)) | ||
Syntax | cli 14831 | Extend class notation with convergence relation for limits. |
class ⇝ | ||
Syntax | crli 14832 | Extend class notation with real convergence relation for limits. |
class ⇝𝑟 | ||
Syntax | co1 14833 | Extend class notation with the set of all eventually bounded functions. |
class 𝑂(1) | ||
Syntax | clo1 14834 | Extend class notation with the set of all eventually upper bounded functions. |
class ≤𝑂(1) | ||
Definition | df-clim 14835* | Define the limit relation for complex number sequences. See clim 14841 for its relational expression. (Contributed by NM, 28-Aug-2005.) |
⊢ ⇝ = {〈𝑓, 𝑦〉 ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))} | ||
Definition | df-rlim 14836* | Define the limit relation for partial functions on the reals. See rlim 14842 for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ ⇝𝑟 = {〈𝑓, 𝑥〉 ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))} | ||
Definition | df-o1 14837* | 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 14838* | 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 14839 | The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ Rel ⇝ | ||
Theorem | rlimrel 14840 | The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014.) |
⊢ Rel ⇝𝑟 | ||
Theorem | clim 14841* | 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 14842* | 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 14843* | Rewrite rlim 14842 for a mapping operation. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.) |
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) | ||
Theorem | rlim2lt 14844* | Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) | ||
Theorem | rlim3 14845* | Restrict the range of the domain bound to reals greater than some 𝐷 ∈ ℝ. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) | ||
Theorem | climcl 14846 | 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 14847 | Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ (ℂ ↑pm ℝ)) | ||
Theorem | rlimf 14848 | Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝐹 ⇝𝑟 𝐴 → 𝐹:dom 𝐹⟶ℂ) | ||
Theorem | rlimss 14849 | Domain closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝐹 ⇝𝑟 𝐴 → dom 𝐹 ⊆ ℝ) | ||
Theorem | rlimcl 14850 | 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 14851* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 14841. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | clim2c 14852* | Express the predicate 𝐹 converges to 𝐴. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝑥)) | ||
Theorem | clim0 14853* | Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘𝐵) < 𝑥))) | ||
Theorem | clim0c 14854* | Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝑥)) | ||
Theorem | rlim0 14855* | Express the predicate 𝐵(𝑧) converges to 0. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.) |
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘𝐵) < 𝑥))) | ||
Theorem | rlim0lt 14856* | 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 14857* | Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝐶)) | ||
Theorem | climi2 14858* | Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝐶) | ||
Theorem | climi0 14859* | 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 14860* | Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 28-Feb-2015.) |
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑅)) | ||
Theorem | rlimi2 14861* | Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑅)) | ||
Theorem | ello1 14862* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ (𝐹 ∈ ≤𝑂(1) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚)) | ||
Theorem | ello12 14863* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ ≤𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚))) | ||
Theorem | ello12r 14864* | Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝑥 → (𝐹‘𝑥) ≤ 𝑀)) → 𝐹 ∈ ≤𝑂(1)) | ||
Theorem | lo1f 14865 | An eventually upper bounded function is a function. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ (𝐹 ∈ ≤𝑂(1) → 𝐹:dom 𝐹⟶ℝ) | ||
Theorem | lo1dm 14866 | An eventually upper bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ (𝐹 ∈ ≤𝑂(1) → dom 𝐹 ⊆ ℝ) | ||
Theorem | lo1bdd 14867* | The defining property of an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ ((𝐹 ∈ ≤𝑂(1) ∧ 𝐹:𝐴⟶ℝ) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚)) | ||
Theorem | ello1mpt 14868* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔ ∃𝑦 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚))) | ||
Theorem | ello1mpt2 14869* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔ ∃𝑦 ∈ (𝐶[,)+∞)∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚))) | ||
Theorem | ello1d 14870* | Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥)) → 𝐵 ≤ 𝑀) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) | ||
Theorem | lo1bdd2 14871* | 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 14872* | Refine o1bdd2 14888 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) & ⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝐵 ≤ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℝ+ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚) | ||
Theorem | elo1 14873* | Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐹 ∈ 𝑂(1) ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚)) | ||
Theorem | elo12 14874* | Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ 𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚))) | ||
Theorem | elo12r 14875* | Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑀)) → 𝐹 ∈ 𝑂(1)) | ||
Theorem | o1f 14876 | An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ) | ||
Theorem | o1dm 14877 | An eventually bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ) | ||
Theorem | o1bdd 14878* | The defining property of an eventually bounded function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:𝐴⟶ℂ) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚)) | ||
Theorem | lo1o1 14879 | 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 14880* | 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 14881* | 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 14882* | 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 14883* | 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 14884* | 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 14885* | 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 14886* | A real eventually bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) | ||
Theorem | icco1 14887* | Derive eventual boundedness from separate upper and lower eventual bounds. (Contributed by Mario Carneiro, 15-Apr-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥)) → 𝐵 ∈ (𝑀[,]𝑁)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) | ||
Theorem | o1bdd2 14888* | 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 14889* | Refine o1bdd2 14888 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) & ⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘𝐵) ≤ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑚) | ||
Theorem | climconst 14890* | An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 𝐴) | ||
Theorem | rlimconst 14891* | A constant sequence converges to its value. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐵) | ||
Theorem | rlimclim1 14892 | Forward direction of rlimclim 14893. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ dom 𝐹) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 𝐴) | ||
Theorem | rlimclim 14893 | 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 14894* | 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 14895 | A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ (ℤ≥‘𝑀) ⊆ 𝑍 & ⊢ 𝑍 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝐴}) ⇝ 𝐴) | ||
Theorem | climz 14896 | The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ (ℤ × {0}) ⇝ 0 | ||
Theorem | rlimuni 14897 | A real function whose domain is unbounded above converges to at most one limit. (Contributed by Mario Carneiro, 8-May-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐵) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) | ||
Theorem | rlimdm 14898 | 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 14899 | 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 14900 | The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.) |
⊢ ⇝ :dom ⇝ ⟶ℂ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |