P. 261 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26001-26100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	limcflf 26001	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 26002*	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 26003*	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 26004*	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 26005	Any limit of 𝐹 is also a limit of the restriction of 𝐹. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ 𝐶) limℂ 𝐵)
Theorem	limcres 26006	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 26007	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 26008*	𝐹 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 26009	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 26010*	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 26011	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 26012*	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 26013*	Composition of two limits. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 ≠ 𝐶)) → 𝑅 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ ((𝑦 ∈ 𝐵 ↦ 𝑆) limℂ 𝐶))    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 = 𝐶)) → 𝑇 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑇) limℂ 𝑋))
Theorem	limciun 26014*	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 26015	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 26016	Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    &   ⊢ (𝜑 → 𝐷 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐷 ∖ {𝐵})) → (((𝐹‘𝐴) − (𝐹‘𝐵)) / (𝐴 − 𝐵)) ∈ ℂ)
Theorem	dvfval 26017*	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 26018*	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 26019	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 26020	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 26021	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 26022	The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ dom (𝑆 D 𝐹) ⊆ 𝑆
Theorem	perfdvf 26023	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 26024	Both ℝ and ℂ are subsets of ℂ. (Contributed by Mario Carneiro, 10-Feb-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Theorem	recnperf 26025	Both ℝ and ℂ are perfect subsets of ℂ. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝐾 ↾t 𝑆) ∈ Perf)
Theorem	dvfg 26026	Explicitly write out the functionality condition on derivative for 𝑆 = ℝ and ℂ. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)
Theorem	dvf 26027	The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
Theorem	dvfcn 26028	The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ
Theorem	dvreslem 26029*	Lemma for dvres 26031. (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 26030*	Lemma for dvres2 26032. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ 𝑇 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)))    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑦 ∈ ℂ)    &   ⊢ (𝜑 → 𝑥(𝑆 D 𝐹)𝑦)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑥(𝐵 D (𝐹 ↾ 𝐵))𝑦)
Theorem	dvres 26031	Restriction of a derivative. Note that our definition of derivative df-dv 25987 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 26032	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 26031, 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 26033	Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015.)
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom (ℂ D 𝐹))) → (𝑆 D (𝐹 ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆))
Theorem	dvres3a 26034	Restriction of a complex differentiable function to the reals. This version of dvres3 26033 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 26035*	Lemma for dvid 26038 and dvconst 26037. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
⊢ (𝜑 → 𝐹:ℂ⟶ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵}))
Theorem	dvmptresicc 26036*	Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (ℂ D 𝐹) = (𝑥 ∈ ℂ ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐶[,]𝐷) ↦ 𝐴)) = (𝑥 ∈ (𝐶(,)𝐷) ↦ 𝐵))
Theorem	dvconst 26037	Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
⊢ (𝐴 ∈ ℂ → (ℂ D (ℂ × {𝐴})) = (ℂ × {0}))
Theorem	dvid 26038	Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
⊢ (ℂ D ( I ↾ ℂ)) = (ℂ × {1})
Theorem	dvcnp 26039*	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 26040	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 11168. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = (𝐾 ↾t 𝐴)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))
Theorem	dvcn 26041	A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ dom (𝑆 D 𝐹) = 𝐴) → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	dvnfval 26042*	Value of the iterated derivative. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑆 D 𝑥))    ⇒   ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹) = seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹})))
Theorem	dvnff 26043	The iterated derivative is a function. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹):ℕ0⟶(ℂ ↑pm dom 𝐹))
Theorem	dvn0 26044	Zero times iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹)
Theorem	dvnp1 26045	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 26046	One times iterated derivative. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹))
Theorem	dvnf 26047	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 26048	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 26049	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 26050	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 26051	Multiple derivative version of dvres3a 26034. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝑁 ∈ ℕ0) ∧ dom ((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))
Theorem	cpnfval 26052*	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 26053	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 26054	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 26055	𝓑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 26056	A 𝓑C𝑛 function is continuous. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ ((𝓑C𝑛‘𝑆)‘𝑁)) → 𝐹 ∈ (dom 𝐹–cn→ℂ))
Theorem	cpnres 26057	The restriction of a 𝓑C𝑛 function is 𝓑C𝑛. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ ((𝓑C𝑛‘ℂ)‘𝑁)) → (𝐹 ↾ 𝑆) ∈ ((𝓑C𝑛‘𝑆)‘𝑁))
Theorem	dvaddbr 26058	The sum rule for derivatives at a point. For the (simpler but more limited) function version, see dvadd 26060. (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 26059	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 26061. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11168 and remove unnecessary hypotheses. (Revised by GG, 16-Mar-2025.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))
Theorem	dvadd 26060	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddbr 26058. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑆 D (𝐹 ∘f + 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘𝐶) + ((𝑆 D 𝐺)‘𝐶)))
Theorem	dvmul 26061	The product rule for derivatives at a point. For the (more general) relation version, see dvmulbr 26059. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑆 D (𝐹 ∘f · 𝐺))‘𝐶) = ((((𝑆 D 𝐹)‘𝐶) · (𝐺‘𝐶)) + (((𝑆 D 𝐺)‘𝐶) · (𝐹‘𝐶))))
Theorem	dvaddf 26062	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 26063	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 26064	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 26065	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 26066	The chain rule for derivatives at a point. For the (simpler but more limited) function version, see dvco 26067. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11168 and remove unnecessary hypotheses. (Revised by GG, 16-Mar-2025.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶𝑋)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑇 ⊆ ℂ)    &   ⊢ (𝜑 → (𝐺‘𝐶)(𝑆 D 𝐹)𝐾)    &   ⊢ (𝜑 → 𝐶(𝑇 D 𝐺)𝐿)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → 𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿))
Theorem	dvco 26067	The chain rule for derivatives at a point. For the (more general) relation version, see dvcobr 26066. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶𝑋)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → (𝐺‘𝐶) ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑇 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑇 D (𝐹 ∘ 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘(𝐺‘𝐶)) · ((𝑇 D 𝐺)‘𝐶)))
Theorem	dvcof 26068	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 26069	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 26070. (This doesn't follow from dvcobr 26066 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 26070	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 26069. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → (ℝ D (∗ ∘ 𝐹)) = (∗ ∘ (ℝ D 𝐹)))
Theorem	dvfre 26071	The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
Theorem	dvnfre 26072	The 𝑁-th derivative of a real function is real. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑁 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑁):dom ((ℝ D𝑛 𝐹)‘𝑁)⟶ℝ)
Theorem	dvexp 26073*	Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
Theorem	dvexp2 26074*	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 26075*	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 26076*	Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑆 ∩ 𝑋) = 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵))
Theorem	dvmptid 26077*	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 26078*	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 26079*	Closure lemma for dvmptcmul 26084 and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ)
Theorem	dvmptadd 26080*	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 26081*	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 26082*	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 26083*	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 26084*	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 26085*	Function-builder for derivative, division rule for constant divisor. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶)))
Theorem	dvmptneg 26086*	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 26087*	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 26088*	Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (∗‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (∗‘𝐵)))
Theorem	dvmptre 26089*	Function-builder for derivative, real part. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐵)))
Theorem	dvmptim 26090*	Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐵)))
Theorem	dvmptntr 26091*	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 26092*	Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷))    &   ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸)    &   ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))
Theorem	dvrecg 26093*	Derivative of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐵)) = (𝑥 ∈ 𝑋 ↦ 𝐶))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵))) = (𝑥 ∈ 𝑋 ↦ -((𝐴 · 𝐶) / (𝐵↑2))))
Theorem	dvmptdiv 26094*	Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (((𝐵 · 𝐶) − (𝐷 · 𝐴)) / (𝐶↑2))))
Theorem	dvmptfsum 26095*	Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵))
Theorem	dvcnvlem 26096	Lemma for dvcnvre 26139. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)    &   ⊢ (𝜑 → ◡𝐹 ∈ (𝑌–cn→𝑋))    &   ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶)(𝑆 D ◡𝐹)(1 / ((𝑆 D 𝐹)‘𝐶)))
Theorem	dvcnv 26097*	A weak version of dvcnvre 26139, valid for both real and complex domains but under the hypothesis that the inverse function is already known to be continuous, and the image set is known to be open. A more advanced proof can show that these conditions are unnecessary. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)    &   ⊢ (𝜑 → ◡𝐹 ∈ (𝑌–cn→𝑋))    &   ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (𝑆 D 𝐹))    ⇒   ⊢ (𝜑 → (𝑆 D ◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((𝑆 D 𝐹)‘(◡𝐹‘𝑥)))))
Theorem	dvexp3 26098*	Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝑁 ∈ ℤ → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥↑𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
Theorem	dveflem 26099	Derivative of the exponential function at 0. The key step in the proof is eftlub 16155, to show that abs(exp(𝑥) − 1 − 𝑥) ≤ abs(𝑥)↑2 · (3 / 4). (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
⊢ 0(ℂ D exp)1
Theorem	dvef 26100	Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
⊢ (ℂ D exp) = exp