![]() |
Metamath
Proof Explorer Theorem List (p. 259 of 483) | < 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-30721) |
![]() (30722-32244) |
![]() (32245-48232) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ellimc3 25801* | Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) | ||
Theorem | limcflflem 25802 | Lemma for limcflf 25803. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴)) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝐶 = (𝐴 ∖ {𝐵}) & ⊢ 𝐿 = (((nei‘𝐾)‘{𝐵}) ↾t 𝐶) ⇒ ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝐶)) | ||
Theorem | limcflf 25803 | 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 25804* | 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 25805* | 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 25806* | 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 25807 | Any limit of 𝐹 is also a limit of the restriction of 𝐹. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ 𝐶) limℂ 𝐵) | ||
Theorem | limcres 25808 | 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 25809 | 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 25810* | 𝐹 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 25811 | 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 25812* | 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 25813 | 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 25814* | 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 25815* | Composition of two limits. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 ≠ 𝐶)) → 𝑅 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝑋)) & ⊢ (𝜑 → 𝐷 ∈ ((𝑦 ∈ 𝐵 ↦ 𝑆) limℂ 𝐶)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 = 𝐶)) → 𝑇 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑇) limℂ 𝑋)) | ||
Theorem | limciun 25816* | 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 25817 | 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 25818 | Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) & ⊢ (𝜑 → 𝐷 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐷 ∖ {𝐵})) → (((𝐹‘𝐴) − (𝐹‘𝐵)) / (𝐴 − 𝐵)) ∈ ℂ) | ||
Theorem | dvfval 25819* | 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 25820* | 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 25821 | 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 25822 | 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 25823 | 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 25824 | The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ dom (𝑆 D 𝐹) ⊆ 𝑆 | ||
Theorem | perfdvf 25825 | 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 25826 | Both ℝ and ℂ are subsets of ℂ. (Contributed by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ) | ||
Theorem | recnperf 25827 | Both ℝ and ℂ are perfect subsets of ℂ. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝐾 ↾t 𝑆) ∈ Perf) | ||
Theorem | dvfg 25828 | Explicitly write out the functionality condition on derivative for 𝑆 = ℝ and ℂ. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) | ||
Theorem | dvf 25829 | The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ | ||
Theorem | dvfcn 25830 | The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ | ||
Theorem | dvreslem 25831* | Lemma for dvres 25833. (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 25832* | Lemma for dvres2 25834. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝑇 = (𝐾 ↾t 𝑆) & ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝐵 ⊆ 𝑆) & ⊢ (𝜑 → 𝑦 ∈ ℂ) & ⊢ (𝜑 → 𝑥(𝑆 D 𝐹)𝑦) & ⊢ (𝜑 → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑥(𝐵 D (𝐹 ↾ 𝐵))𝑦) | ||
Theorem | dvres 25833 | Restriction of a derivative. Note that our definition of derivative df-dv 25789 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 25834 | 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 25833, 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 25835 | Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015.) |
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom (ℂ D 𝐹))) → (𝑆 D (𝐹 ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆)) | ||
Theorem | dvres3a 25836 | Restriction of a complex differentiable function to the reals. This version of dvres3 25835 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 25837* | Lemma for dvid 25840 and dvconst 25839. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵) & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵})) | ||
Theorem | dvmptresicc 25838* | Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (ℂ D 𝐹) = (𝑥 ∈ ℂ ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐶[,]𝐷) ↦ 𝐴)) = (𝑥 ∈ (𝐶(,)𝐷) ↦ 𝐵)) | ||
Theorem | dvconst 25839 | Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝐴 ∈ ℂ → (ℂ D (ℂ × {𝐴})) = (ℂ × {0})) | ||
Theorem | dvid 25840 | Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
⊢ (ℂ D ( I ↾ ℂ)) = (ℂ × {1}) | ||
Theorem | dvcnp 25841* | 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 25842 | 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.) Avoid ax-mulf 11212. (Revised by GG, 16-Mar-2025.) |
⊢ 𝐽 = (𝐾 ↾t 𝐴) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) | ||
Theorem | dvcnp2OLD 25843 | Obsolete version of dvcnp2 25842 as of 10-Apr-2025. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐽 = (𝐾 ↾t 𝐴) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) | ||
Theorem | dvcn 25844 | A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.) |
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ dom (𝑆 D 𝐹) = 𝐴) → 𝐹 ∈ (𝐴–cn→ℂ)) | ||
Theorem | dvnfval 25845* | Value of the iterated derivative. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑆 D 𝑥)) ⇒ ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹) = seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹}))) | ||
Theorem | dvnff 25846 | The iterated derivative is a function. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹):ℕ0⟶(ℂ ↑pm dom 𝐹)) | ||
Theorem | dvn0 25847 | Zero times iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) | ||
Theorem | dvnp1 25848 | 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 25849 | One times iterated derivative. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹)) | ||
Theorem | dvnf 25850 | 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 25851 | 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 25852 | 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 25853 | 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 25854 | Multiple derivative version of dvres3a 25836. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝑁 ∈ ℕ0) ∧ dom ((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) | ||
Theorem | cpnfval 25855* | Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝑆 ⊆ ℂ → (𝓑C𝑛‘𝑆) = (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑆) ∣ ((𝑆 D𝑛 𝑓)‘𝑛) ∈ (dom 𝑓–cn→ℂ)})) | ||
Theorem | fncpn 25856 | The 𝓑C𝑛 object is a function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝑆 ⊆ ℂ → (𝓑C𝑛‘𝑆) Fn ℕ0) | ||
Theorem | elcpn 25857 | Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐹 ∈ ((𝓑C𝑛‘𝑆)‘𝑁) ↔ (𝐹 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (dom 𝐹–cn→ℂ)))) | ||
Theorem | cpnord 25858 | 𝓑C𝑛 conditions are ordered by strength. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → ((𝓑C𝑛‘𝑆)‘𝑁) ⊆ ((𝓑C𝑛‘𝑆)‘𝑀)) | ||
Theorem | cpncn 25859 | A 𝓑C𝑛 function is continuous. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ ((𝓑C𝑛‘𝑆)‘𝑁)) → 𝐹 ∈ (dom 𝐹–cn→ℂ)) | ||
Theorem | cpnres 25860 | The restriction of a 𝓑C𝑛 function is 𝓑C𝑛. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ ((𝓑C𝑛‘ℂ)‘𝑁)) → (𝐹 ↾ 𝑆) ∈ ((𝓑C𝑛‘𝑆)‘𝑁)) | ||
Theorem | dvaddbr 25861 | The sum rule for derivatives at a point. For the (simpler but more limited) function version, see dvadd 25864. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Remove unnecessary hypotheses. (Revised by GG, 10-Apr-2025.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝐺:𝑌⟶ℂ) & ⊢ (𝜑 → 𝑌 ⊆ 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾) & ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿) & ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘f + 𝐺))(𝐾 + 𝐿)) | ||
Theorem | dvmulbr 25862 | The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 25865. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11212 and remove unnecessary hypotheses. (Revised by GG, 16-Mar-2025.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝐺:𝑌⟶ℂ) & ⊢ (𝜑 → 𝑌 ⊆ 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾) & ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿) & ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶)))) | ||
Theorem | dvmulbrOLD 25863 | Obsolete version of dvmulbr 25862 as of 10-Apr-2025. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝐺:𝑌⟶ℂ) & ⊢ (𝜑 → 𝑌 ⊆ 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾) & ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿) & ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶)))) | ||
Theorem | dvadd 25864 | The sum rule for derivatives at a point. For the (more general) relation version, see dvaddbr 25861. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝐺:𝑌⟶ℂ) & ⊢ (𝜑 → 𝑌 ⊆ 𝑆) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹)) & ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺)) ⇒ ⊢ (𝜑 → ((𝑆 D (𝐹 ∘f + 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘𝐶) + ((𝑆 D 𝐺)‘𝐶))) | ||
Theorem | dvmul 25865 | The product rule for derivatives at a point. For the (more general) relation version, see dvmulbr 25862. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝐺:𝑌⟶ℂ) & ⊢ (𝜑 → 𝑌 ⊆ 𝑆) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹)) & ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺)) ⇒ ⊢ (𝜑 → ((𝑆 D (𝐹 ∘f · 𝐺))‘𝐶) = ((((𝑆 D 𝐹)‘𝐶) · (𝐺‘𝐶)) + (((𝑆 D 𝐺)‘𝐶) · (𝐹‘𝐶)))) | ||
Theorem | dvaddf 25866 | The sum rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) & ⊢ (𝜑 → dom (𝑆 D 𝐺) = 𝑋) ⇒ ⊢ (𝜑 → (𝑆 D (𝐹 ∘f + 𝐺)) = ((𝑆 D 𝐹) ∘f + (𝑆 D 𝐺))) | ||
Theorem | dvmulf 25867 | The product rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) & ⊢ (𝜑 → dom (𝑆 D 𝐺) = 𝑋) ⇒ ⊢ (𝜑 → (𝑆 D (𝐹 ∘f · 𝐺)) = (((𝑆 D 𝐹) ∘f · 𝐺) ∘f + ((𝑆 D 𝐺) ∘f · 𝐹))) | ||
Theorem | dvcmul 25868 | The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹)) ⇒ ⊢ (𝜑 → ((𝑆 D ((𝑆 × {𝐴}) ∘f · 𝐹))‘𝐶) = (𝐴 · ((𝑆 D 𝐹)‘𝐶))) | ||
Theorem | dvcmulf 25869 | The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) ⇒ ⊢ (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ∘f · 𝐹)) = ((𝑆 × {𝐴}) ∘f · (𝑆 D 𝐹))) | ||
Theorem | dvcobr 25870 | The chain rule for derivatives at a point. For the (simpler but more limited) function version, see dvco 25872. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11212 and remove unnecessary hypotheses. (Revised by GG, 16-Mar-2025.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝐺:𝑌⟶𝑋) & ⊢ (𝜑 → 𝑌 ⊆ 𝑇) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑇 ⊆ ℂ) & ⊢ (𝜑 → (𝐺‘𝐶)(𝑆 D 𝐹)𝐾) & ⊢ (𝜑 → 𝐶(𝑇 D 𝐺)𝐿) & ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → 𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿)) | ||
Theorem | dvcobrOLD 25871 | Obsolete version of dvcobr 25870 as of 10-Apr-2025. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝐺:𝑌⟶𝑋) & ⊢ (𝜑 → 𝑌 ⊆ 𝑇) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑇 ⊆ ℂ) & ⊢ (𝜑 → (𝐺‘𝐶)(𝑆 D 𝐹)𝐾) & ⊢ (𝜑 → 𝐶(𝑇 D 𝐺)𝐿) & ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → 𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿)) | ||
Theorem | dvco 25872 | The chain rule for derivatives at a point. For the (more general) relation version, see dvcobr 25870. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝐺:𝑌⟶𝑋) & ⊢ (𝜑 → 𝑌 ⊆ 𝑇) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → (𝐺‘𝐶) ∈ dom (𝑆 D 𝐹)) & ⊢ (𝜑 → 𝐶 ∈ dom (𝑇 D 𝐺)) ⇒ ⊢ (𝜑 → ((𝑇 D (𝐹 ∘ 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘(𝐺‘𝐶)) · ((𝑇 D 𝐺)‘𝐶))) | ||
Theorem | dvcof 25873 | The chain rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 10-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐺:𝑌⟶𝑋) & ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) & ⊢ (𝜑 → dom (𝑇 D 𝐺) = 𝑌) ⇒ ⊢ (𝜑 → (𝑇 D (𝐹 ∘ 𝐺)) = (((𝑆 D 𝐹) ∘ 𝐺) ∘f · (𝑇 D 𝐺))) | ||
Theorem | dvcjbr 25874 | The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 25875. (This doesn't follow from dvcobr 25870 because ∗ is not a function on the reals, and even if we used complex derivatives, ∗ is not complex-differentiable.) (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ dom (ℝ D 𝐹)) ⇒ ⊢ (𝜑 → 𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶))) | ||
Theorem | dvcj 25875 | The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 25874. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → (ℝ D (∗ ∘ 𝐹)) = (∗ ∘ (ℝ D 𝐹))) | ||
Theorem | dvfre 25876 | The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) | ||
Theorem | dvnfre 25877 | The 𝑁-th derivative of a real function is real. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑁 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑁):dom ((ℝ D𝑛 𝐹)‘𝑁)⟶ℝ) | ||
Theorem | dvexp 25878* | Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) | ||
Theorem | dvexp2 25879* | Derivative of an exponential, possibly zero power. (Contributed by Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝑁 ∈ ℕ0 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))))) | ||
Theorem | dvrec 25880* | Derivative of the reciprocal function. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.) |
⊢ (𝐴 ∈ ℂ → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2)))) | ||
Theorem | dvmptres3 25881* | Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ (𝜑 → (𝑆 ∩ 𝑋) = 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵)) | ||
Theorem | dvmptid 25882* | Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑆 ↦ 𝑥)) = (𝑥 ∈ 𝑆 ↦ 1)) | ||
Theorem | dvmptc 25883* | Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 0)) | ||
Theorem | dvmptcl 25884* | Closure lemma for dvmptcmul 25889 and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ) | ||
Theorem | dvmptadd 25885* | Function-builder for derivative, addition rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 + 𝐷))) | ||
Theorem | dvmptmul 25886* | Function-builder for derivative, product rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐶))) = (𝑥 ∈ 𝑋 ↦ ((𝐵 · 𝐶) + (𝐷 · 𝐴)))) | ||
Theorem | dvmptres2 25887* | Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → 𝑍 ⊆ 𝑋) & ⊢ 𝐽 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → ((int‘𝐽)‘𝑍) = 𝑌) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑍 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵)) | ||
Theorem | dvmptres 25888* | Function-builder for derivative: restrict a derivative to an open subset. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ 𝐽 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝑌 ∈ 𝐽) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵)) | ||
Theorem | dvmptcmul 25889* | Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐶 · 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝐶 · 𝐵))) | ||
Theorem | dvmptdivc 25890* | Function-builder for derivative, division rule for constant divisor. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶))) | ||
Theorem | dvmptneg 25891* | Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ -𝐴)) = (𝑥 ∈ 𝑋 ↦ -𝐵)) | ||
Theorem | dvmptsub 25892* | Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 − 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 − 𝐷))) | ||
Theorem | dvmptcj 25893* | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (∗‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (∗‘𝐵))) | ||
Theorem | dvmptre 25894* | Function-builder for derivative, real part. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐵))) | ||
Theorem | dvmptim 25895* | Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐵))) | ||
Theorem | dvmptntr 25896* | Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ 𝐽 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → ((int‘𝐽)‘𝑋) = 𝑌) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴))) | ||
Theorem | dvmptco 25897* | Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷)) & ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸) & ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵))) | ||
Theorem | dvrecg 25898* | Derivative of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐵)) = (𝑥 ∈ 𝑋 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵))) = (𝑥 ∈ 𝑋 ↦ -((𝐴 · 𝐶) / (𝐵↑2)))) | ||
Theorem | dvmptdiv 25899* | Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ ℂ) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (((𝐵 · 𝐶) − (𝐷 · 𝐴)) / (𝐶↑2)))) | ||
Theorem | dvmptfsum 25900* | Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
⊢ 𝐽 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |