P. 250 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	itgmulc2lem1 24901*	Lemma for itgmulc2 24903: positive real case. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgmulc2lem2 24902*	Lemma for itgmulc2 24903: real case. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgmulc2 24903*	Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgabs 24904*	The triangle inequality for integrals. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (abs‘∫𝐴𝐵 d𝑥) ≤ ∫𝐴(abs‘𝐵) d𝑥)
Theorem	itgsplit 24905*	The ∫ integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0)    &   ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝑈𝐶 d𝑥 = (∫𝐴𝐶 d𝑥 + ∫𝐵𝐶 d𝑥))
Theorem	itgspliticc 24906*	The ∫ integral splits on closed intervals with matching endpoints. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐶)) → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶) ↦ 𝐷) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫(𝐴[,]𝐶)𝐷 d𝑥 = (∫(𝐴[,]𝐵)𝐷 d𝑥 + ∫(𝐵[,]𝐶)𝐷 d𝑥))
Theorem	itgsplitioo 24907*	The ∫ integral splits on open intervals with matching endpoints. (Contributed by Mario Carneiro, 2-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐶)) → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐷) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐵(,)𝐶) ↦ 𝐷) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥))
Theorem	bddmulibl 24908*	A bounded function times an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ ((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝐹 ∘f · 𝐺) ∈ 𝐿1)
Theorem	bddibl 24909*	A bounded function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1)
Theorem	cniccibl 24910	A continuous function on a closed bounded interval is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿1)
Theorem	bddiblnc 24911*	Choice-free proof of bddibl 24909. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.)
⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1)
Theorem	cnicciblnc 24912	Choice-free proof of cniccibl 24910. (Contributed by Brendan Leahy, 2-Nov-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿1)
Theorem	itggt0 24913*	The integral of a strictly positive function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ (𝜑 → 0 < (vol‘𝐴))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 0 < ∫𝐴𝐵 d𝑥)
Theorem	itgcn 24914*	Transfer itg2cn 24833 to the full Lebesgue integral. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐴 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘𝐵) d𝑥 < 𝐶))
13.2.2.2  Lesbesgue directed integral
Syntax	cdit 24915	Extend class notation with the directed integral.
class ⨜[𝐴 → 𝐵]𝐶 d𝑥
Definition	df-ditg 24916	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 24917*	Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝐴 = 𝐵 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = ⨜[𝐵 → 𝐶]𝐷 d𝑥)
Theorem	ditgeq2 24918*	Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝐴 = 𝐵 → ⨜[𝐶 → 𝐴]𝐷 d𝑥 = ⨜[𝐶 → 𝐵]𝐷 d𝑥)
Theorem	ditgeq3 24919*	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 24925 first and use the equality theorems for df-itg 24692.) (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (∀𝑥 ∈ ℝ 𝐷 = 𝐸 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ⨜[𝐴 → 𝐵]𝐸 d𝑥)
Theorem	ditgeq3dv 24920*	Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐷 = 𝐸)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ⨜[𝐴 → 𝐵]𝐸 d𝑥)
Theorem	ditgex 24921	A directed integral is a set. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 ∈ V
Theorem	ditg0 24922*	Value of the directed integral from a point to itself. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ⨜[𝐴 → 𝐴]𝐵 d𝑥 = 0
Theorem	cbvditg 24923*	Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦
Theorem	cbvditgv 24924*	Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦
Theorem	ditgpos 24925*	Value of the directed integral in the forward direction. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ∫(𝐴(,)𝐵)𝐶 d𝑥)
Theorem	ditgneg 24926*	Value of the directed integral in the backward direction. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ⨜[𝐵 → 𝐴]𝐶 d𝑥 = -∫(𝐴(,)𝐵)𝐶 d𝑥)
Theorem	ditgcl 24927*	Closure of a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 ∈ ℂ)
Theorem	ditgswap 24928*	Reverse a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ⨜[𝐵 → 𝐴]𝐶 d𝑥 = -⨜[𝐴 → 𝐵]𝐶 d𝑥)
Theorem	ditgsplitlem 24929*	Lemma for ditgsplit 24930. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑋[,]𝑌))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ 𝐿1)    &   ⊢ ((𝜓 ∧ 𝜃) ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
Theorem	ditgsplit 24930*	This theorem is the raison d'être for the directed integral, because unlike itgspliticc 24906, there is no constraint on the ordering of the points 𝐴, 𝐵, 𝐶 in the domain. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑋[,]𝑌))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
13.3  Derivatives
13.3.1  Real and complex differentiation
13.3.1.1  Derivatives of functions of one complex or real variable
Syntax	climc 24931	The limit operator.
class limℂ
Syntax	cdv 24932	The derivative operator.
class D
Syntax	cdvn 24933	The 𝑛-th derivative operator.
class D𝑛
Syntax	ccpn 24934	The set of 𝑛-times continuously differentiable functions.
class 𝓑C𝑛
Definition	df-limc 24935*	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 24936*	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 24937*	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 24938*	Define the set of 𝑛-times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014.)
⊢ 𝓑C𝑛 = (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}))
Theorem	reldv 24939	The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ Rel (𝑆 D 𝐹)
Theorem	limcvallem 24940*	Lemma for ellimc 24942. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵}))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))    ⇒   ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐵) → 𝐶 ∈ ℂ))
Theorem	limcfval 24941*	Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵}))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∧ (𝐹 limℂ 𝐵) ⊆ ℂ))
Theorem	ellimc 24942*	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 24943	Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐶 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
Theorem	limccl 24944	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝐹 limℂ 𝐵) ⊆ ℂ
Theorem	limcdif 24945	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 24946*	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 24947	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 24948*	Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))
Theorem	limcflflem 24949	Lemma for limcflf 24950. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ 𝐶 = (𝐴 ∖ {𝐵})    &   ⊢ 𝐿 = (((nei‘𝐾)‘{𝐵}) ↾t 𝐶)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝐶))
Theorem	limcflf 24950	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 24951*	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 24952*	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 24953*	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 24954	Any limit of 𝐹 is also a limit of the restriction of 𝐹. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ 𝐶) limℂ 𝐵)
Theorem	limcres 24955	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 24956	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 24957*	𝐹 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 24958	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 24959*	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 24960	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 24961*	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 24962*	Composition of two limits. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 ≠ 𝐶)) → 𝑅 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ ((𝑦 ∈ 𝐵 ↦ 𝑆) limℂ 𝐶))    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 = 𝐶)) → 𝑇 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑇) limℂ 𝑋))
Theorem	limciun 24963*	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 24964	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 24965	Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    &   ⊢ (𝜑 → 𝐷 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐷 ∖ {𝐵})) → (((𝐹‘𝐴) − (𝐹‘𝐵)) / (𝐴 − 𝐵)) ∈ ℂ)
Theorem	dvfval 24966*	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 24967*	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 24968	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 24969	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 24970	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 24971	The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ dom (𝑆 D 𝐹) ⊆ 𝑆
Theorem	perfdvf 24972	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 24973	Both ℝ and ℂ are subsets of ℂ. (Contributed by Mario Carneiro, 10-Feb-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Theorem	recnperf 24974	Both ℝ and ℂ are perfect subsets of ℂ. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝐾 ↾t 𝑆) ∈ Perf)
Theorem	dvfg 24975	Explicitly write out the functionality condition on derivative for 𝑆 = ℝ and ℂ. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)
Theorem	dvf 24976	The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
Theorem	dvfcn 24977	The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ
Theorem	dvreslem 24978*	Lemma for dvres 24980. (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 24979*	Lemma for dvres2 24981. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ 𝑇 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)))    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑦 ∈ ℂ)    &   ⊢ (𝜑 → 𝑥(𝑆 D 𝐹)𝑦)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑥(𝐵 D (𝐹 ↾ 𝐵))𝑦)
Theorem	dvres 24980	Restriction of a derivative. Note that our definition of derivative df-dv 24936 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 24981	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 24980, 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 24982	Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015.)
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℂ ∧ 𝑆 ⊆ dom (ℂ D 𝐹))) → (𝑆 D (𝐹 ↾ 𝑆)) = ((ℂ D 𝐹) ↾ 𝑆))
Theorem	dvres3a 24983	Restriction of a complex differentiable function to the reals. This version of dvres3 24982 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 24984*	Lemma for dvid 24987 and dvconst 24986. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
⊢ (𝜑 → 𝐹:ℂ⟶ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵}))
Theorem	dvmptresicc 24985*	Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (ℂ D 𝐹) = (𝑥 ∈ ℂ ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐶[,]𝐷) ↦ 𝐴)) = (𝑥 ∈ (𝐶(,)𝐷) ↦ 𝐵))
Theorem	dvconst 24986	Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
⊢ (𝐴 ∈ ℂ → (ℂ D (ℂ × {𝐴})) = (ℂ × {0}))
Theorem	dvid 24987	Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
⊢ (ℂ D ( I ↾ ℂ)) = (ℂ × {1})
Theorem	dvcnp 24988*	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 24989	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 24990	A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ dom (𝑆 D 𝐹) = 𝐴) → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	dvnfval 24991*	Value of the iterated derivative. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑆 D 𝑥))    ⇒   ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹) = seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹})))
Theorem	dvnff 24992	The iterated derivative is a function. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹):ℕ0⟶(ℂ ↑pm dom 𝐹))
Theorem	dvn0 24993	Zero times iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹)
Theorem	dvnp1 24994	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 24995	One times iterated derivative. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹))
Theorem	dvnf 24996	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 24997	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 24998	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 24999	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 25000	Multiple derivative version of dvres3a 24983. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝑁 ∈ ℕ0) ∧ dom ((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))