Home | Metamath
Proof Explorer Theorem List (p. 142 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ello1mpt2 14101* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔ ∃𝑦 ∈ (𝐶[,)+∞)∃𝑚 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚))) | ||
Theorem | ello1d 14102* | Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥)) → 𝐵 ≤ 𝑀) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) | ||
Theorem | lo1bdd2 14103* | 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 14104* | Refine o1bdd2 14120 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) & ⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝐵 ≤ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℝ+ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑚) | ||
Theorem | elo1 14105* | Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐹 ∈ 𝑂(1) ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚)) | ||
Theorem | elo12 14106* | Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ 𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚))) | ||
Theorem | elo12r 14107* | Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑀)) → 𝐹 ∈ 𝑂(1)) | ||
Theorem | o1f 14108 | An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ) | ||
Theorem | o1dm 14109 | An eventually bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ) | ||
Theorem | o1bdd 14110* | The defining property of an eventually bounded function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:𝐴⟶ℂ) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚)) | ||
Theorem | lo1o1 14111 | 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 14112* | 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 14113* | 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 14114* | 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 14115* | 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 14116* | 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 14117* | 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 14118* | A real eventually bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) | ||
Theorem | icco1 14119* | Derive eventual boundedness from separate upper and lower eventual bounds. (Contributed by Mario Carneiro, 15-Apr-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥)) → 𝐵 ∈ (𝑀[,]𝑁)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) | ||
Theorem | o1bdd2 14120* | 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 14121* | Refine o1bdd2 14120 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) & ⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦)) → 𝑀 ∈ ℝ) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ((𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘𝐵) ≤ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑚) | ||
Theorem | climconst 14122* | An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 𝐴) | ||
Theorem | rlimconst 14123* | A constant sequence converges to its value. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐵) | ||
Theorem | rlimclim1 14124 | Forward direction of rlimclim 14125. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ dom 𝐹) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 𝐴) | ||
Theorem | rlimclim 14125 | 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 14126* | 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 14127 | A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ (ℤ≥‘𝑀) ⊆ 𝑍 & ⊢ 𝑍 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝐴}) ⇝ 𝐴) | ||
Theorem | climz 14128 | The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ (ℤ × {0}) ⇝ 0 | ||
Theorem | rlimuni 14129 | A real function whose domain is unbounded above converges to at most one limit. (Contributed by Mario Carneiro, 8-May-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐵) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) | ||
Theorem | rlimdm 14130 | 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 14131 | 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 14132 | The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.) |
⊢ ⇝ :dom ⇝ ⟶ℂ | ||
Theorem | climdm 14133 | 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 14134* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.) |
⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 𝐹 ⇝ 𝑥) | ||
Theorem | climreu 14135* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.) |
⊢ (𝐹 ⇝ 𝐴 → ∃!𝑥 ∈ ℂ 𝐹 ⇝ 𝑥) | ||
Theorem | climmo 14136* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.) |
⊢ ∃*𝑥 𝐹 ⇝ 𝑥 | ||
Theorem | rlimres 14137 | The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝐹 ⇝𝑟 𝐴 → (𝐹 ↾ 𝐵) ⇝𝑟 𝐴) | ||
Theorem | lo1res 14138 | The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐹 ∈ ≤𝑂(1) → (𝐹 ↾ 𝐴) ∈ ≤𝑂(1)) | ||
Theorem | o1res 14139 | 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 14140* | The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ⇝𝑟 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷) | ||
Theorem | lo1res2 14141* | The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ ≤𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1)) | ||
Theorem | o1res2 14142* | The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1)) | ||
Theorem | lo1resb 14143 | 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 14144 | The restriction of a function to an unbounded-above interval converges iff the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐹 ⇝𝑟 𝐶 ↔ (𝐹 ↾ (𝐵[,)+∞)) ⇝𝑟 𝐶)) | ||
Theorem | o1resb 14145 | 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 14146* | 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 14147* | 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 14148* | Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥)) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐸 ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸)) | ||
Theorem | o1eq 14149* | 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 14150* | Exhibit a function 𝐺 with the same convergence properties as the not-quite-function 𝐹. (Contributed by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐺 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴)) | ||
Theorem | 2clim 14151* | 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 14152* | Relate an integer limit on a not-quite-function to a real limit. (Contributed by Mario Carneiro, 17-Sep-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝑛 ∈ 𝑍 ↦ (𝐹‘𝑛)) ⇝𝑟 𝐴)) | ||
Theorem | climshftlem 14153 | A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝑀 ∈ ℤ → (𝐹 ⇝ 𝐴 → (𝐹 shift 𝑀) ⇝ 𝐴)) | ||
Theorem | climres 14154 | 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 14155 | 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 14156 | 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 14157* | 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 14158* | 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 14159* | The limit of a real sequence is real. (Contributed by Mario Carneiro, 9-May-2016.) |
⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐶 ∈ ℝ) | ||
Theorem | rlimge0 14160* | The limit of a sequence of nonnegative reals is nonnegative. (Contributed by Mario Carneiro, 10-May-2016.) |
⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ 𝐶) | ||
Theorem | climshft2 14161* | 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 14162* | 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 14163* | 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 14164* | 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 14165* | Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐹 ∈ 𝑂(1)) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦))) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ 𝑂(1)) | ||
Theorem | o1compt 14166* | Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐹 ∈ 𝑂(1)) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘ (𝑦 ∈ 𝐵 ↦ 𝐶)) ∈ 𝑂(1)) | ||
Theorem | rlimcn1 14167* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014.) |
⊢ (𝜑 → 𝐺:𝐴⟶𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ⇝𝑟 𝐶) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝𝑟 (𝐹‘𝐶)) | ||
Theorem | rlimcn1b 14168* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 10-May-2016.) |
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥)) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)) ⇝𝑟 (𝐹‘𝐶)) | ||
Theorem | rlimcn2 14169* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌) & ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝑅) & ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝑆) & ⊢ (𝜑 → 𝐹:(𝑋 × 𝑌)⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) ⇒ ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ (𝐵𝐹𝐶)) ⇝𝑟 (𝑅𝐹𝑆)) | ||
Theorem | climcn1 14170* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) ∈ ℂ) & ⊢ (𝜑 → 𝐺 ⇝ 𝐴) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐵 ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) < 𝑥)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐹‘𝐴)) | ||
Theorem | climcn2 14171* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐶 ∧ 𝑣 ∈ 𝐷)) → (𝑢𝐹𝑣) ∈ ℂ) & ⊢ (𝜑 → 𝐺 ⇝ 𝐴) & ⊢ (𝜑 → 𝐻 ⇝ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐾‘𝑘) = ((𝐺‘𝑘)𝐹(𝐻‘𝑘))) ⇒ ⊢ (𝜑 → 𝐾 ⇝ (𝐴𝐹𝐵)) | ||
Theorem | addcn2 14172* | 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 20841 and df-cncf 22489 are not yet available to us. See addcn 22476 for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) | ||
Theorem | subcn2 14173* | 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 14174* | 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 14175* | 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 14176* | A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
⊢ 𝐹:ℂ⟶ℂ & ⊢ ((𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) ≤ (abs‘(𝑧 − 𝐴))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) < 𝑥)) | ||
Theorem | abscn2 14177* | The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((abs‘𝑧) − (abs‘𝐴))) < 𝑥)) | ||
Theorem | cjcn2 14178* | The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((∗‘𝑧) − (∗‘𝐴))) < 𝑥)) | ||
Theorem | recn2 14179* | The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((ℜ‘𝑧) − (ℜ‘𝐴))) < 𝑥)) | ||
Theorem | imcn2 14180* | The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((ℑ‘𝑧) − (ℑ‘𝐴))) < 𝑥)) | ||
Theorem | climcn1lem 14181* | The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ 𝐻:ℂ⟶ℂ & ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐻‘𝑧) − (𝐻‘𝐴))) < 𝑥)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐻‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (𝐻‘𝐴)) | ||
Theorem | climabs 14182* | 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 14183* | 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 14184* | 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 14185* | 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 14186* | Reverse closure for a real limit. (Contributed by Mario Carneiro, 10-May-2016.) |
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) | ||
Theorem | rlimabs 14187* | 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 14188* | 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 14189* | 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 14190* | 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 14191* | Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈ ℝ) & ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝑅𝑦) ∈ ℂ) & ⊢ (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) ⇒ ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (𝐹 ∘𝑓 𝑅𝐺) ∈ 𝑂(1)) | ||
Theorem | o1add 14192 | 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)) → (𝐹 ∘𝑓 + 𝐺) ∈ 𝑂(1)) | ||
Theorem | o1mul 14193 | 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)) → (𝐹 ∘𝑓 · 𝐺) ∈ 𝑂(1)) | ||
Theorem | o1sub 14194 | 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)) → (𝐹 ∘𝑓 − 𝐺) ∈ 𝑂(1)) | ||
Theorem | rlimo1 14195 | Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ 𝑂(1)) | ||
Theorem | rlimdmo1 14196 | A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ (𝐹 ∈ dom ⇝𝑟 → 𝐹 ∈ 𝑂(1)) | ||
Theorem | o1rlimmul 14197 | 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) → (𝐹 ∘𝑓 · 𝐺) ⇝𝑟 0) | ||
Theorem | o1const 14198* | A constant function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) | ||
Theorem | lo1const 14199* | A constant function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) | ||
Theorem | lo1mptrcl 14200* | Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |