Home | Metamath
Proof Explorer Theorem List (p. 248 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | itgmulc2lem1 24701* | Lemma for itgmulc2 24703: positive real case. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgmulc2lem2 24702* | Lemma for itgmulc2 24703: real case. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgmulc2 24703* | Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgabs 24704* | The triangle inequality for integrals. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → (abs‘∫𝐴𝐵 d𝑥) ≤ ∫𝐴(abs‘𝐵) d𝑥) | ||
Theorem | itgsplit 24705* | The ∫ integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) & ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫𝑈𝐶 d𝑥 = (∫𝐴𝐶 d𝑥 + ∫𝐵𝐶 d𝑥)) | ||
Theorem | itgspliticc 24706* | The ∫ integral splits on closed intervals with matching endpoints. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐶)) → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶) ↦ 𝐷) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫(𝐴[,]𝐶)𝐷 d𝑥 = (∫(𝐴[,]𝐵)𝐷 d𝑥 + ∫(𝐵[,]𝐶)𝐷 d𝑥)) | ||
Theorem | itgsplitioo 24707* | The ∫ integral splits on open intervals with matching endpoints. (Contributed by Mario Carneiro, 2-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐶)) → 𝐷 ∈ ℂ) & ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐷) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ (𝐵(,)𝐶) ↦ 𝐷) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) | ||
Theorem | bddmulibl 24708* | A bounded function times an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ ((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝐹 ∘f · 𝐺) ∈ 𝐿1) | ||
Theorem | bddibl 24709* | A bounded function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1) | ||
Theorem | cniccibl 24710 | A continuous function on a closed bounded interval is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿1) | ||
Theorem | bddiblnc 24711* | Choice-free proof of bddibl 24709. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.) |
⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1) | ||
Theorem | cnicciblnc 24712 | Choice-free proof of cniccibl 24710. (Contributed by Brendan Leahy, 2-Nov-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿1) | ||
Theorem | itggt0 24713* | The integral of a strictly positive function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.) |
⊢ (𝜑 → 0 < (vol‘𝐴)) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → 0 < ∫𝐴𝐵 d𝑥) | ||
Theorem | itgcn 24714* | Transfer itg2cn 24633 to the full Lebesgue integral. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐴 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘𝐵) d𝑥 < 𝐶)) | ||
Syntax | cdit 24715 | Extend class notation with the directed integral. |
class ⨜[𝐴 → 𝐵]𝐶 d𝑥 | ||
Definition | df-ditg 24716 | Define the directed integral, which is just a regular integral but with a sign change when the limits are interchanged. The 𝐴 and 𝐵 here are the lower and upper limits of the integral, usually written as a subscript and superscript next to the integral sign. We define the region of integration to be an open interval instead of closed so that we can use +∞, -∞ for limits and also integrate up to a singularity at an endpoint. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = if(𝐴 ≤ 𝐵, ∫(𝐴(,)𝐵)𝐶 d𝑥, -∫(𝐵(,)𝐴)𝐶 d𝑥) | ||
Theorem | ditgeq1 24717* | Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝐴 = 𝐵 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = ⨜[𝐵 → 𝐶]𝐷 d𝑥) | ||
Theorem | ditgeq2 24718* | Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝐴 = 𝐵 → ⨜[𝐶 → 𝐴]𝐷 d𝑥 = ⨜[𝐶 → 𝐵]𝐷 d𝑥) | ||
Theorem | ditgeq3 24719* | Equality theorem for the directed integral. (The domain of the equality here is very rough; for more precise bounds one should decompose it with ditgpos 24725 first and use the equality theorems for df-itg 24492.) (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (∀𝑥 ∈ ℝ 𝐷 = 𝐸 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ⨜[𝐴 → 𝐵]𝐸 d𝑥) | ||
Theorem | ditgeq3dv 24720* | Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐷 = 𝐸) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ⨜[𝐴 → 𝐵]𝐸 d𝑥) | ||
Theorem | ditgex 24721 | A directed integral is a set. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 ∈ V | ||
Theorem | ditg0 24722* | Value of the directed integral from a point to itself. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ⨜[𝐴 → 𝐴]𝐵 d𝑥 = 0 | ||
Theorem | cbvditg 24723* | Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 ⇒ ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦 | ||
Theorem | cbvditgv 24724* | Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦 | ||
Theorem | ditgpos 24725* | Value of the directed integral in the forward direction. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ∫(𝐴(,)𝐵)𝐶 d𝑥) | ||
Theorem | ditgneg 24726* | Value of the directed integral in the backward direction. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ⨜[𝐵 → 𝐴]𝐶 d𝑥 = -∫(𝐴(,)𝐵)𝐶 d𝑥) | ||
Theorem | ditgcl 24727* | Closure of a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 ∈ ℂ) | ||
Theorem | ditgswap 24728* | Reverse a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ⨜[𝐵 → 𝐴]𝐶 d𝑥 = -⨜[𝐴 → 𝐵]𝐶 d𝑥) | ||
Theorem | ditgsplitlem 24729* | Lemma for ditgsplit 24730. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐶 ∈ (𝑋[,]𝑌)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ 𝐿1) & ⊢ ((𝜓 ∧ 𝜃) ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥)) | ||
Theorem | ditgsplit 24730* | This theorem is the raison d'être for the directed integral, because unlike itgspliticc 24706, there is no constraint on the ordering of the points 𝐴, 𝐵, 𝐶 in the domain. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐶 ∈ (𝑋[,]𝑌)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥)) | ||
Syntax | climc 24731 | The limit operator. |
class limℂ | ||
Syntax | cdv 24732 | The derivative operator. |
class D | ||
Syntax | cdvn 24733 | The 𝑛-th derivative operator. |
class D𝑛 | ||
Syntax | ccpn 24734 | The set of 𝑛-times continuously differentiable functions. |
class 𝓑C𝑛 | ||
Definition | df-limc 24735* | Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ limℂ = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∣ [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)}) | ||
Definition | df-dv 24736* | Define the derivative operator. This acts on functions to produce a function that is defined where the original function is differentiable, with value the derivative of the function at these points. The set 𝑠 here is the ambient topological space under which we are evaluating the continuity of the difference quotient. Although the definition is valid for any subset of ℂ and is well-behaved when 𝑠 contains no isolated points, we will restrict our attention to the cases 𝑠 = ℝ or 𝑠 = ℂ for the majority of the development, these corresponding respectively to real and complex differentiation. (Contributed by Mario Carneiro, 7-Aug-2014.) |
⊢ D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ ∪ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) | ||
Definition | df-dvn 24737* | Define the 𝑛-th derivative operator on functions on the complex numbers. This just iterates the derivative operation according to the last argument. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))) | ||
Definition | df-cpn 24738* | Define the set of 𝑛-times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
⊢ 𝓑C𝑛 = (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)})) | ||
Theorem | reldv 24739 | The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ Rel (𝑆 D 𝐹) | ||
Theorem | limcvallem 24740* | Lemma for ellimc 24742. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ⇒ ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐵) → 𝐶 ∈ ℂ)) | ||
Theorem | limcfval 24741* | Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∧ (𝐹 limℂ 𝐵) ⊆ ℂ)) | ||
Theorem | ellimc 24742* | Value of the limit predicate. 𝐶 is the limit of the function 𝐹 at 𝐵 if the function 𝐺, formed by adding 𝐵 to the domain of 𝐹 and setting it to 𝐶, is continuous at 𝐵. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐵))) | ||
Theorem | limcrcl 24743 | Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝐶 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ)) | ||
Theorem | limccl 24744 | Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝐹 limℂ 𝐵) ⊆ ℂ | ||
Theorem | limcdif 24745 | It suffices to consider functions which are not defined at 𝐵 to define the limit of a function. In particular, the value of the original function 𝐹 at 𝐵 does not affect the limit of 𝐹. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝐹 ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵)) | ||
Theorem | ellimc2 24746* | Write the definition of a limit directly in terms of open sets of the topology on the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝐶 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))) | ||
Theorem | limcnlp 24747 | If 𝐵 is not a limit point of the domain of the function 𝐹, then every point is a limit of 𝐹 at 𝐵. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → ¬ 𝐵 ∈ ((limPt‘𝐾)‘𝐴)) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ℂ) | ||
Theorem | ellimc3 24748* | Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) | ||
Theorem | limcflflem 24749 | Lemma for limcflf 24750. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴)) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐶 = (𝐴 ∖ {𝐵}) & ⊢ 𝐿 = (((nei‘𝐾)‘{𝐵}) ↾t 𝐶) ⇒ ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝐶)) | ||
Theorem | limcflf 24750 | The limit operator can be expressed as a filter limit, from the filter of neighborhoods of 𝐵 restricted to 𝐴 ∖ {𝐵}, to the topology of the complex numbers. (If 𝐵 is not a limit point of 𝐴, then it is still formally a filter limit, but the neighborhood filter is not a proper filter in this case.) (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴)) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐶 = (𝐴 ∖ {𝐵}) & ⊢ 𝐿 = (((nei‘𝐾)‘{𝐵}) ↾t 𝐶) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝐾 fLimf 𝐿)‘(𝐹 ↾ 𝐶))) | ||
Theorem | limcmo 24751* | If 𝐵 is a limit point of the domain of the function 𝐹, then there is at most one limit value of 𝐹 at 𝐵. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴)) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐹 limℂ 𝐵)) | ||
Theorem | limcmpt 24752* | Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐷 ∈ ℂ) & ⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → (𝐶 ∈ ((𝑧 ∈ 𝐴 ↦ 𝐷) limℂ 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, 𝐷)) ∈ ((𝐽 CnP 𝐾)‘𝐵))) | ||
Theorem | limcmpt2 24753* | Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵)) → 𝐷 ∈ ℂ) & ⊢ 𝐽 = (𝐾 ↾t 𝐴) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → (𝐶 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ 𝐷) limℂ 𝐵) ↔ (𝑧 ∈ 𝐴 ↦ if(𝑧 = 𝐵, 𝐶, 𝐷)) ∈ ((𝐽 CnP 𝐾)‘𝐵))) | ||
Theorem | limcresi 24754 | Any limit of 𝐹 is also a limit of the restriction of 𝐹. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ 𝐶) limℂ 𝐵) | ||
Theorem | limcres 24755 | If 𝐵 is an interior point of 𝐶 ∪ {𝐵} relative to the domain 𝐴, then a limit point of 𝐹 ↾ 𝐶 extends to a limit of 𝐹. (Contributed by Mario Carneiro, 27-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) & ⊢ (𝜑 → 𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵}))) ⇒ ⊢ (𝜑 → ((𝐹 ↾ 𝐶) limℂ 𝐵) = (𝐹 limℂ 𝐵)) | ||
Theorem | cnplimc 24756 | A function is continuous at 𝐵 iff its limit at 𝐵 equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐽 = (𝐾 ↾t 𝐴) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵)))) | ||
Theorem | cnlimc 24757* | 𝐹 is a continuous function iff the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝐴 ⊆ ℂ → (𝐹 ∈ (𝐴–cn→ℂ) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ (𝐹 limℂ 𝑥)))) | ||
Theorem | cnlimci 24758 | If 𝐹 is a continuous function, then the limit of the function at any point equals its value. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐷)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵)) | ||
Theorem | cnmptlimc 24759* | If 𝐹 is a continuous function, then the limit of the function at any point equals its value. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑋) ∈ (𝐴–cn→𝐷)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝑥 = 𝐵 → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → 𝑌 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑋) limℂ 𝐵)) | ||
Theorem | limccnp 24760 | If the limit of 𝐹 at 𝐵 is 𝐶 and 𝐺 is continuous at 𝐶, then the limit of 𝐺 ∘ 𝐹 at 𝐵 is 𝐺(𝐶). (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℂ) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐽 = (𝐾 ↾t 𝐷) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐵)) & ⊢ (𝜑 → 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐶)) ⇒ ⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝐺 ∘ 𝐹) limℂ 𝐵)) | ||
Theorem | limccnp2 24761* | The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 ∈ 𝑌) & ⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑌 ⊆ ℂ) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐽 = ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) & ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵)) & ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑆) limℂ 𝐵)) & ⊢ (𝜑 → 𝐻 ∈ ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉)) ⇒ ⊢ (𝜑 → (𝐶𝐻𝐷) ∈ ((𝑥 ∈ 𝐴 ↦ (𝑅𝐻𝑆)) limℂ 𝐵)) | ||
Theorem | limcco 24762* | Composition of two limits. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 ≠ 𝐶)) → 𝑅 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝑋)) & ⊢ (𝜑 → 𝐷 ∈ ((𝑦 ∈ 𝐵 ↦ 𝑆) limℂ 𝐶)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 = 𝐶)) → 𝑇 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑇) limℂ 𝑋)) | ||
Theorem | limciun 24763* | A point is a limit of 𝐹 on the finite union ∪ 𝑥 ∈ 𝐴𝐵(𝑥) iff it is the limit of the restriction of 𝐹 to each 𝐵(𝑥). (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐶) = (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶))) | ||
Theorem | limcun 24764 | A point is a limit of 𝐹 on 𝐴 ∪ 𝐵 iff it is the limit of the restriction of 𝐹 to 𝐴 and to 𝐵. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:(𝐴 ∪ 𝐵)⟶ℂ) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐶) = (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶))) | ||
Theorem | dvlem 24765 | Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) & ⊢ (𝜑 → 𝐷 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐷 ∖ {𝐵})) → (((𝐹‘𝐴) − (𝐹‘𝐵)) / (𝐴 − 𝐵)) ∈ ℂ) | ||
Theorem | dvfval 24766* | Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑇 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → ((𝑆 D 𝐹) = ∪ 𝑥 ∈ ((int‘𝑇)‘𝐴)({𝑥} × ((𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)) ∧ (𝑆 D 𝐹) ⊆ (((int‘𝑇)‘𝐴) × ℂ))) | ||
Theorem | eldv 24767* | The differentiable predicate. A function 𝐹 is differentiable at 𝐵 with derivative 𝐶 iff 𝐹 is defined in a neighborhood of 𝐵 and the difference quotient has limit 𝐶 at 𝐵. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑇 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐵(𝑆 D 𝐹)𝐶 ↔ (𝐵 ∈ ((int‘𝑇)‘𝐴) ∧ 𝐶 ∈ (𝐺 limℂ 𝐵)))) | ||
Theorem | dvcl 24768 | The derivative function takes values in the complex numbers. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝐵(𝑆 D 𝐹)𝐶) → 𝐶 ∈ ℂ) | ||
Theorem | dvbssntr 24769 | The set of differentiable points is a subset of the interior of the domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ 𝐽 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ ((int‘𝐽)‘𝐴)) | ||
Theorem | dvbss 24770 | The set of differentiable points is a subset of the domain of the function. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) ⇒ ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝐴) | ||
Theorem | dvbsss 24771 | The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ dom (𝑆 D 𝐹) ⊆ 𝑆 | ||
Theorem | perfdvf 24772 | The derivative is a function, whenever it is defined relative to a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝐾 ↾t 𝑆) ∈ Perf → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) | ||
Theorem | recnprss 24773 | Both ℝ and ℂ are subsets of ℂ. (Contributed by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ) | ||
Theorem | recnperf 24774 | Both ℝ and ℂ are perfect subsets of ℂ. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝐾 ↾t 𝑆) ∈ Perf) | ||
Theorem | dvfg 24775 | Explicitly write out the functionality condition on derivative for 𝑆 = ℝ and ℂ. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) | ||
Theorem | dvf 24776 | The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ | ||
Theorem | dvfcn 24777 | The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ | ||
Theorem | dvreslem 24778* | Lemma for dvres 24780. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Commute the consequent and shorten proof. (Revised by Peter Mazsa, 2-Oct-2022.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝑇 = (𝐾 ↾t 𝑆) & ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝐵 ⊆ 𝑆) & ⊢ (𝜑 → 𝑦 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐵) ∧ 𝑥(𝑆 D 𝐹)𝑦))) | ||
Theorem | dvres2lem 24779* | Lemma for dvres2 24781. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝑇 = (𝐾 ↾t 𝑆) & ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝐵 ⊆ 𝑆) & ⊢ (𝜑 → 𝑦 ∈ ℂ) & ⊢ (𝜑 → 𝑥(𝑆 D 𝐹)𝑦) & ⊢ (𝜑 → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑥(𝐵 D (𝐹 ↾ 𝐵))𝑦) | ||
Theorem | dvres 24780 | Restriction of a derivative. Note that our definition of derivative df-dv 24736 would still make sense if we demanded that 𝑥 be an element of the domain instead of an interior point of the domain, but then it is possible for a non-differentiable function to have two different derivatives at a single point 𝑥 when restricted to different subsets containing 𝑥; a classic example is the absolute value function restricted to [0, +∞) and (-∞, 0]. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝑇 = (𝐾 ↾t 𝑆) ⇒ ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → (𝑆 D (𝐹 ↾ 𝐵)) = ((𝑆 D 𝐹) ↾ ((int‘𝑇)‘𝐵))) | ||
Theorem | dvres2 24781 | Restriction of the base set of a derivative. The primary application of this theorem says that if a function is complex-differentiable then it is also real-differentiable. Unlike dvres 24780, there is no simple reverse relation relating real-differentiable functions to complex differentiability, and indeed there are functions like ℜ(𝑥) which are everywhere real-differentiable but nowhere complex-differentiable.) (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆)) → ((𝑆 D 𝐹) ↾ 𝐵) ⊆ (𝐵 D (𝐹 ↾ 𝐵))) | ||
Theorem | dvres3 24782 | Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015.) |
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom (ℂ D 𝐹))) → (𝑆 D (𝐹 ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆)) | ||
Theorem | dvres3a 24783 | Restriction of a complex differentiable function to the reals. This version of dvres3 24782 assumes that 𝐹 is differentiable on its domain, but does not require 𝐹 to be differentiable on the whole real line. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ∈ 𝐽 ∧ dom (ℂ D 𝐹) = 𝐴)) → (𝑆 D (𝐹 ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆)) | ||
Theorem | dvidlem 24784* | Lemma for dvid 24787 and dvconst 24786. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵) & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵})) | ||
Theorem | dvmptresicc 24785* | Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (ℂ D 𝐹) = (𝑥 ∈ ℂ ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐶[,]𝐷) ↦ 𝐴)) = (𝑥 ∈ (𝐶(,)𝐷) ↦ 𝐵)) | ||
Theorem | dvconst 24786 | Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝐴 ∈ ℂ → (ℂ D (ℂ × {𝐴})) = (ℂ × {0})) | ||
Theorem | dvid 24787 | Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (ℂ D ( I ↾ ℂ)) = (ℂ × {1}) | ||
Theorem | dvcnp 24788* | The difference quotient is continuous at 𝐵 when the original function is differentiable at 𝐵. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐽 = (𝐾 ↾t 𝐴) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐺 = (𝑧 ∈ 𝐴 ↦ if(𝑧 = 𝐵, ((𝑆 D 𝐹)‘𝐵), (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)))) ⇒ ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐵)) | ||
Theorem | dvcnp2 24789 | A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐽 = (𝐾 ↾t 𝐴) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) | ||
Theorem | dvcn 24790 | A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.) |
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ dom (𝑆 D 𝐹) = 𝐴) → 𝐹 ∈ (𝐴–cn→ℂ)) | ||
Theorem | dvnfval 24791* | Value of the iterated derivative. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑆 D 𝑥)) ⇒ ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹) = seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹}))) | ||
Theorem | dvnff 24792 | The iterated derivative is a function. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹):ℕ0⟶(ℂ ↑pm dom 𝐹)) | ||
Theorem | dvn0 24793 | Zero times iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) | ||
Theorem | dvnp1 24794 | Successor iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ 𝑁 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑁))) | ||
Theorem | dvn1 24795 | One times iterated derivative. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹)) | ||
Theorem | dvnf 24796 | The N-times derivative is a function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ 𝑁 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ) | ||
Theorem | dvnbss 24797 | The set of N-times differentiable points is a subset of the domain of the function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ 𝑁 ∈ ℕ0) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom 𝐹) | ||
Theorem | dvnadd 24798 | The 𝑁-th derivative of the 𝑀-th derivative of 𝐹 is the same as the 𝑀 + 𝑁-th derivative of 𝐹. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁))) | ||
Theorem | dvn2bss 24799 | An N-times differentiable point is an M-times differentiable point, if 𝑀 ≤ 𝑁. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ 𝑀 ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘𝑀)) | ||
Theorem | dvnres 24800 | Multiple derivative version of dvres3a 24783. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝑁 ∈ ℕ0) ∧ dom ((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |