Home | Metamath
Proof Explorer Theorem List (p. 235 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 | iblabs 23401* | The absolute value of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1) | ||
Theorem | iblabsr 23402* | A measurable function is integrable iff its absolute value is integrable. (See iblabs 23401 for the forward implication.) (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) | ||
Theorem | iblmulc2 23403* | Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1) | ||
Theorem | itgmulc2lem1 23404* | Lemma for itgmulc2 23406: positive real case. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgmulc2lem2 23405* | Lemma for itgmulc2 23406: real case. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgmulc2 23406* | Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgabs 23407* | The triangle inequality for integrals. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → (abs‘∫𝐴𝐵 d𝑥) ≤ ∫𝐴(abs‘𝐵) d𝑥) | ||
Theorem | itgsplit 23408* | The ∫ integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) & ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫𝑈𝐶 d𝑥 = (∫𝐴𝐶 d𝑥 + ∫𝐵𝐶 d𝑥)) | ||
Theorem | itgspliticc 23409* | The ∫ integral splits on closed intervals with matching endpoints. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐶)) → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶) ↦ 𝐷) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫(𝐴[,]𝐶)𝐷 d𝑥 = (∫(𝐴[,]𝐵)𝐷 d𝑥 + ∫(𝐵[,]𝐶)𝐷 d𝑥)) | ||
Theorem | itgsplitioo 23410* | The ∫ integral splits on open intervals with matching endpoints. (Contributed by Mario Carneiro, 2-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐶)) → 𝐷 ∈ ℂ) & ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐷) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ (𝐵(,)𝐶) ↦ 𝐷) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) | ||
Theorem | bddmulibl 23411* | A bounded function times an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ ((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝐹 ∘𝑓 · 𝐺) ∈ 𝐿1) | ||
Theorem | bddibl 23412* | A bounded function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1) | ||
Theorem | cniccibl 23413 | A continuous function on a closed bounded interval is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿1) | ||
Theorem | itggt0 23414* | The integral of a strictly positive function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.) |
⊢ (𝜑 → 0 < (vol‘𝐴)) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → 0 < ∫𝐴𝐵 d𝑥) | ||
Theorem | itgcn 23415* | Transfer itg2cn 23336 to the full Lebesgue integral. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐴 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘𝐵) d𝑥 < 𝐶)) | ||
Syntax | cdit 23416 | Extend class notation with the directed integral. |
class ⨜[𝐴 → 𝐵]𝐶 d𝑥 | ||
Definition | df-ditg 23417 | 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 23418* | Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝐴 = 𝐵 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = ⨜[𝐵 → 𝐶]𝐷 d𝑥) | ||
Theorem | ditgeq2 23419* | Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝐴 = 𝐵 → ⨜[𝐶 → 𝐴]𝐷 d𝑥 = ⨜[𝐶 → 𝐵]𝐷 d𝑥) | ||
Theorem | ditgeq3 23420* | 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 23426 first and use the equality theorems for df-itg 23198.) (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (∀𝑥 ∈ ℝ 𝐷 = 𝐸 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ⨜[𝐴 → 𝐵]𝐸 d𝑥) | ||
Theorem | ditgeq3dv 23421* | Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐷 = 𝐸) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ⨜[𝐴 → 𝐵]𝐸 d𝑥) | ||
Theorem | ditgex 23422 | A directed integral is a set. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 ∈ V | ||
Theorem | ditg0 23423* | Value of the directed integral from a point to itself. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ⨜[𝐴 → 𝐴]𝐵 d𝑥 = 0 | ||
Theorem | cbvditg 23424* | Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 ⇒ ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦 | ||
Theorem | cbvditgv 23425* | Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦 | ||
Theorem | ditgpos 23426* | Value of the directed integral in the forward direction. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ∫(𝐴(,)𝐵)𝐶 d𝑥) | ||
Theorem | ditgneg 23427* | Value of the directed integral in the backward direction. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ⨜[𝐵 → 𝐴]𝐶 d𝑥 = -∫(𝐴(,)𝐵)𝐶 d𝑥) | ||
Theorem | ditgcl 23428* | Closure of a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 ∈ ℂ) | ||
Theorem | ditgswap 23429* | Reverse a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ⨜[𝐵 → 𝐴]𝐶 d𝑥 = -⨜[𝐴 → 𝐵]𝐶 d𝑥) | ||
Theorem | ditgsplitlem 23430* | Lemma for ditgsplit 23431. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐶 ∈ (𝑋[,]𝑌)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ 𝐿1) & ⊢ ((𝜓 ∧ 𝜃) ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥)) | ||
Theorem | ditgsplit 23431* | This theorem is the raison d'être for the directed integral, because unlike itgspliticc 23409, 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 23432 | The limit operator. |
class limℂ | ||
Syntax | cdv 23433 | The derivative operator. |
class D | ||
Syntax | cdvn 23434 | The 𝑛-th derivative operator. |
class D𝑛 | ||
Syntax | ccpn 23435 | The set of 𝑛-times continuously differentiable functions. |
class Cn | ||
Definition | df-limc 23436* | 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 23437* | Define the derivative operator on functions on the reals. 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 23438* | 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 23439* | Define the set of 𝑛-times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
⊢ Cn = (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)})) | ||
Theorem | reldv 23440 | The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ Rel (𝑆 D 𝐹) | ||
Theorem | limcvallem 23441* | Lemma for ellimc 23443. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ⇒ ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐵) → 𝐶 ∈ ℂ)) | ||
Theorem | limcfval 23442* | Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∧ (𝐹 limℂ 𝐵) ⊆ ℂ)) | ||
Theorem | ellimc 23443* | 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 23444 | Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝐶 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ)) | ||
Theorem | limccl 23445 | Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝐹 limℂ 𝐵) ⊆ ℂ | ||
Theorem | limcdif 23446 | 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 23447* | 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 23448 | 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 23449* | Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) | ||
Theorem | limcflflem 23450 | Lemma for limcflf 23451. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴)) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐶 = (𝐴 ∖ {𝐵}) & ⊢ 𝐿 = (((nei‘𝐾)‘{𝐵}) ↾t 𝐶) ⇒ ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝐶)) | ||
Theorem | limcflf 23451 | 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 23452* | 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 23453* | 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 23454* | 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 23455 | Any limit of 𝐹 is also a limit of the restriction of 𝐹. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ 𝐶) limℂ 𝐵) | ||
Theorem | limcres 23456 | 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 23457 | 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 23458* | 𝐹 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 23459 | 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 23460* | 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 23461 | 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 23462* | 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 23463* | Composition of two limits. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 ≠ 𝐶)) → 𝑅 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝑋)) & ⊢ (𝜑 → 𝐷 ∈ ((𝑦 ∈ 𝐵 ↦ 𝑆) limℂ 𝐶)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 = 𝐶)) → 𝑇 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑇) limℂ 𝑋)) | ||
Theorem | limciun 23464* | 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 23465 | 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 23466 | Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) & ⊢ (𝜑 → 𝐷 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐷 ∖ {𝐵})) → (((𝐹‘𝐴) − (𝐹‘𝐵)) / (𝐴 − 𝐵)) ∈ ℂ) | ||
Theorem | dvfval 23467* | 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 23468* | 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 23469 | 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 23470 | 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 23471 | 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 23472 | The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ dom (𝑆 D 𝐹) ⊆ 𝑆 | ||
Theorem | perfdvf 23473 | 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 23474 | Both ℝ and ℂ are subsets of ℂ. (Contributed by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ) | ||
Theorem | recnperf 23475 | Both ℝ and ℂ are perfect subsets of ℂ. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝐾 ↾t 𝑆) ∈ Perf) | ||
Theorem | dvfg 23476 | Explicitly write out the functionality condition on derivative for 𝑆 = ℝ and ℂ. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) | ||
Theorem | dvf 23477 | The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ | ||
Theorem | dvfcn 23478 | The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ | ||
Theorem | dvreslem 23479* | Lemma for dvres 23481. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝑇 = (𝐾 ↾t 𝑆) & ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝐵 ⊆ 𝑆) & ⊢ (𝜑 → 𝑦 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑥(𝑆 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥(𝑆 D 𝐹)𝑦 ∧ 𝑥 ∈ ((int‘𝑇)‘𝐵)))) | ||
Theorem | dvres2lem 23480* | Lemma for dvres2 23482. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝑇 = (𝐾 ↾t 𝑆) & ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝐵 ⊆ 𝑆) & ⊢ (𝜑 → 𝑦 ∈ ℂ) & ⊢ (𝜑 → 𝑥(𝑆 D 𝐹)𝑦) & ⊢ (𝜑 → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑥(𝐵 D (𝐹 ↾ 𝐵))𝑦) | ||
Theorem | dvres 23481 | Restriction of a derivative. Note that our definition of derivative df-dv 23437 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 23482 | 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 23481, 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 23483 | Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015.) |
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom (ℂ D 𝐹))) → (𝑆 D (𝐹 ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆)) | ||
Theorem | dvres3a 23484 | Restriction of a complex differentiable function to the reals. This version of dvres3 23483 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 23485* | Lemma for dvid 23487 and dvconst 23486. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵) & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵})) | ||
Theorem | dvconst 23486 | Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝐴 ∈ ℂ → (ℂ D (ℂ × {𝐴})) = (ℂ × {0})) | ||
Theorem | dvid 23487 | Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (ℂ D ( I ↾ ℂ)) = (ℂ × {1}) | ||
Theorem | dvcnp 23488* | 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 23489 | 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 23490 | A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.) |
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ dom (𝑆 D 𝐹) = 𝐴) → 𝐹 ∈ (𝐴–cn→ℂ)) | ||
Theorem | dvnfval 23491* | Value of the iterated derivative. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑆 D 𝑥)) ⇒ ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹) = seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹}))) | ||
Theorem | dvnff 23492 | The iterated derivative is a function. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹):ℕ0⟶(ℂ ↑pm dom 𝐹)) | ||
Theorem | dvn0 23493 | Zero times iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) | ||
Theorem | dvnp1 23494 | 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 23495 | One times iterated derivative. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹)) | ||
Theorem | dvnf 23496 | 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 23497 | 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 23498 | 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 23499 | 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 23500 | Multiple derivative version of dvres3a 23484. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝑁 ∈ ℕ0) ∧ dom ((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |