| Metamath
Proof Explorer Theorem List (p. 156 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | reusq0 15501* | 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 15502 | 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 15503 | 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 15504 | 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 15502, 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 15505 | 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 15506 | Extend class notation to include the limsup function. |
| class lim sup | ||
| Definition | df-limsup 15507* | Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 15510 for its value. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 11-Sep-2020.) |
| ⊢ lim sup = (𝑥 ∈ V ↦ inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < )) | ||
| Theorem | limsupgord 15508 | 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 15509 | Closure of the superior limit. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 12-Sep-2020.) |
| ⊢ (𝐹 ∈ 𝑉 → (lim sup‘𝐹) ∈ ℝ*) | ||
| Theorem | limsupval 15510* | 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 15511* | Closure of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
| ⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ 𝐺:ℝ⟶ℝ* | ||
| Theorem | limsupgval 15512* | Value of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
| ⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ (𝑀 ∈ ℝ → (𝐺‘𝑀) = sup(((𝐹 “ (𝑀[,)+∞)) ∩ ℝ*), ℝ*, < )) | ||
| Theorem | limsupgle 15513* | 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 15514* | 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 15515* | 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 15516* | 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 15517* | 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 15518* | 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 15519* | 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 15520 | Extend class notation with convergence relation for limits. |
| class ⇝ | ||
| Syntax | crli 15521 | Extend class notation with real convergence relation for limits. |
| class ⇝𝑟 | ||
| Syntax | co1 15522 | Extend class notation with the set of all eventually bounded functions. |
| class 𝑂(1) | ||
| Syntax | clo1 15523 | Extend class notation with the set of all eventually upper bounded functions. |
| class ≤𝑂(1) | ||
| Definition | df-clim 15524* | Define the limit relation for complex number sequences. See clim 15530 for its relational expression. (Contributed by NM, 28-Aug-2005.) |
| ⊢ ⇝ = {〈𝑓, 𝑦〉 ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))} | ||
| Definition | df-rlim 15525* | Define the limit relation for partial functions on the reals. See rlim 15531 for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014.) |
| ⊢ ⇝𝑟 = {〈𝑓, 𝑥〉 ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))} | ||
| Definition | df-o1 15526* | 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 15527* | 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 15528 | The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| ⊢ Rel ⇝ | ||
| Theorem | rlimrel 15529 | The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014.) |
| ⊢ Rel ⇝𝑟 | ||
| Theorem | clim 15530* | 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 15531* | 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 15532* | Rewrite rlim 15531 for a mapping operation. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.) |
| ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) | ||
| Theorem | rlim2lt 15533* | Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.) |
| ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) | ||
| Theorem | rlim3 15534* | Restrict the range of the domain bound to reals greater than some 𝐷 ∈ ℝ. (Contributed by Mario Carneiro, 16-Sep-2014.) |
| ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) | ||
| Theorem | climcl 15535 | 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 15536 | Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
| ⊢ (𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ (ℂ ↑pm ℝ)) | ||
| Theorem | rlimf 15537 | Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
| ⊢ (𝐹 ⇝𝑟 𝐴 → 𝐹:dom 𝐹⟶ℂ) | ||
| Theorem | rlimss 15538 | Domain closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
| ⊢ (𝐹 ⇝𝑟 𝐴 → dom 𝐹 ⊆ ℝ) | ||
| Theorem | rlimcl 15539 | 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 15540* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 15530. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
| Theorem | clim2c 15541* | Express the predicate 𝐹 converges to 𝐴. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝑥)) | ||
| Theorem | clim0 15542* | Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘𝐵) < 𝑥))) | ||
| Theorem | clim0c 15543* | Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝑥)) | ||
| Theorem | rlim0 15544* | Express the predicate 𝐵(𝑧) converges to 0. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.) |
| ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘𝐵) < 𝑥))) | ||
| Theorem | rlim0lt 15545* | 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 15546* | Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝐶)) | ||
| Theorem | climi2 15547* | Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝐶) | ||
| Theorem | climi0 15548* | 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 15549* | Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 28-Feb-2015.) |
| ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑅)) | ||
| Theorem | rlimi2 15550* | Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑅)) | ||
| Theorem | ello1 15551* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ (𝐹 ∈ ≤𝑂(1) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚)) | ||
| Theorem | ello12 15552* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ ≤𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚))) | ||
| Theorem | ello12r 15553* | Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝑥 → (𝐹‘𝑥) ≤ 𝑀)) → 𝐹 ∈ ≤𝑂(1)) | ||
| Theorem | lo1f 15554 | An eventually upper bounded function is a function. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ (𝐹 ∈ ≤𝑂(1) → 𝐹:dom 𝐹⟶ℝ) | ||
| Theorem | lo1dm 15555 | An eventually upper bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ (𝐹 ∈ ≤𝑂(1) → dom 𝐹 ⊆ ℝ) | ||
| Theorem | lo1bdd 15556* | The defining property of an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ ((𝐹 ∈ ≤𝑂(1) ∧ 𝐹:𝐴⟶ℝ) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ 𝑚)) | ||
| Theorem | ello1mpt 15557* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔ ∃𝑦 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚))) | ||
| Theorem | ello1mpt2 15558* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔ ∃𝑦 ∈ (𝐶[,)+∞)∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚))) | ||
| Theorem | ello1d 15559* | Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥)) → 𝐵 ≤ 𝑀) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) | ||
| Theorem | lo1bdd2 15560* | 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 15561* | Refine o1bdd2 15577 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) & ⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝐵 ≤ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℝ+ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚) | ||
| Theorem | elo1 15562* | Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ (𝐹 ∈ 𝑂(1) ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚)) | ||
| Theorem | elo12 15563* | Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ 𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚))) | ||
| Theorem | elo12r 15564* | Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑀)) → 𝐹 ∈ 𝑂(1)) | ||
| Theorem | o1f 15565 | An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ) | ||
| Theorem | o1dm 15566 | An eventually bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ) | ||
| Theorem | o1bdd 15567* | The defining property of an eventually bounded function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:𝐴⟶ℂ) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚)) | ||
| Theorem | lo1o1 15568 | 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 15569* | 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 15570* | 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 15571* | 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 15572* | 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 15573* | 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 15574* | 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 15575* | A real eventually bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) | ||
| Theorem | icco1 15576* | Derive eventual boundedness from separate upper and lower eventual bounds. (Contributed by Mario Carneiro, 15-Apr-2016.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥)) → 𝐵 ∈ (𝑀[,]𝑁)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) | ||
| Theorem | o1bdd2 15577* | 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 15578* | Refine o1bdd2 15577 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) & ⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘𝐵) ≤ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑚) | ||
| Theorem | climconst 15579* | An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 𝐴) | ||
| Theorem | rlimconst 15580* | A constant sequence converges to its value. (Contributed by Mario Carneiro, 16-Sep-2014.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐵) | ||
| Theorem | rlimclim1 15581 | Forward direction of rlimclim 15582. (Contributed by Mario Carneiro, 16-Sep-2014.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ dom 𝐹) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 𝐴) | ||
| Theorem | rlimclim 15582 | 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 15583* | 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 15584 | A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| ⊢ (ℤ≥‘𝑀) ⊆ 𝑍 & ⊢ 𝑍 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝐴}) ⇝ 𝐴) | ||
| Theorem | climz 15585 | The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.) |
| ⊢ (ℤ × {0}) ⇝ 0 | ||
| Theorem | rlimuni 15586 | A real function whose domain is unbounded above converges to at most one limit. (Contributed by Mario Carneiro, 8-May-2016.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐵) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) | ||
| Theorem | rlimdm 15587 | 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 15588 | 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 15589 | The limit relation is function-like, and with codomain the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.) |
| ⊢ ⇝ :dom ⇝ ⟶ℂ | ||
| Theorem | climdm 15590 | 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 15591* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.) |
| ⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 𝐹 ⇝ 𝑥) | ||
| Theorem | climreu 15592* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.) |
| ⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 ∈ ℂ 𝐹 ⇝ 𝑥) | ||
| Theorem | climmo 15593* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.) |
| ⊢ ∃*𝑥 𝐹 ⇝ 𝑥 | ||
| Theorem | rlimres 15594 | The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
| ⊢ (𝐹 ⇝𝑟 𝐴 → (𝐹 ↾ 𝐵) ⇝𝑟 𝐴) | ||
| Theorem | lo1res 15595 | The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ (𝐹 ∈ ≤𝑂(1) → (𝐹 ↾ 𝐴) ∈ ≤𝑂(1)) | ||
| Theorem | o1res 15596 | 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 15597* | The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ⇝𝑟 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷) | ||
| Theorem | lo1res2 15598* | The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 26-May-2016.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ ≤𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1)) | ||
| Theorem | o1res2 15599* | The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 21-May-2016.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1)) | ||
| Theorem | lo1resb 15600 | 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))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |