P. 156 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15501-15600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ivthdec 15501*	The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑦) < (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivthreinc 15502*	Restating the intermediate value theorem. Given a hypothesis stating the intermediate value theorem (in a strong form which is not provable given our axioms alone), provide a conclusion similar to the theorem as stated in the Metamath Proof Explorer (which is also similar to how we state the theorem for a strictly monotonic function at ivthinc 15500). Being able to have a hypothesis stating the intermediate value theorem will be helpful when it comes time to show that it implies a constructive taboo. This version of the theorem requires that the function 𝐹 is continuous on the entire real line, not just (𝐴[,]𝐵) which may be an unnecessary condition but which is sufficient for the way we want to use it. (Contributed by Jim Kingdon, 7-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (ℝ–cn→ℝ))    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (𝜑 → ∀𝑓(𝑓 ∈ (ℝ–cn→ℝ) → ∀𝑎 ∈ ℝ ∀𝑏 ∈ ℝ ((𝑎 < 𝑏 ∧ (𝑓‘𝑎) < 0 ∧ 0 < (𝑓‘𝑏)) → ∃𝑥 ∈ ℝ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ∧ (𝑓‘𝑥) = 0))))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	hovercncf 15503	The hover function is continuous. By hover function, we mean a a function which starts out as a line of slope one, is constant at zero from zero to one, and then resumes as a slope of one. (Contributed by Jim Kingdon, 20-Jul-2025.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   ⊢ 𝐹 ∈ (ℝ–cn→ℝ)
Theorem	hovera 15504*	A point at which the hover function is less than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   ⊢ (𝑍 ∈ ℝ → (𝐹‘(𝑍 − 1)) < 𝑍)
Theorem	hoverb 15505*	A point at which the hover function is greater than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   ⊢ (𝑍 ∈ ℝ → 𝑍 < (𝐹‘(𝑍 + 2)))
Theorem	hoverlt1 15506*	The hover function evaluated at a point less than one. (Contributed by Jim Kingdon, 22-Jul-2025.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   ⊢ ((𝐶 ∈ ℝ ∧ 𝐶 < 1) → (𝐹‘𝐶) ≤ 0)
Theorem	hovergt0 15507*	The hover function evaluated at a point greater than zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   ⊢ ((𝐶 ∈ ℝ ∧ 0 < 𝐶) → 0 ≤ (𝐹‘𝐶))
Theorem	ivthdichlem 15508*	Lemma for ivthdich 15510. The result, with a few notational conveniences. (Contributed by Jim Kingdon, 22-Jul-2025.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    &   ⊢ (𝜑 → 𝑍 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑓(𝑓 ∈ (ℝ–cn→ℝ) → ∀𝑎 ∈ ℝ ∀𝑏 ∈ ℝ ((𝑎 < 𝑏 ∧ (𝑓‘𝑎) < 0 ∧ 0 < (𝑓‘𝑏)) → ∃𝑥 ∈ ℝ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ∧ (𝑓‘𝑥) = 0))))    ⇒   ⊢ (𝜑 → (𝑍 ≤ 0 ∨ 0 ≤ 𝑍))
Theorem	dich0 15509*	Real number dichotomy stated in terms of two real numbers or a real number and zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
⊢ (∀𝑧 ∈ ℝ (𝑧 ≤ 0 ∨ 0 ≤ 𝑧) ↔ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))
Theorem	ivthdich 15510*	The intermediate value theorem implies real number dichotomy. Because real number dichotomy (also known as analytic LLPO) is a constructive taboo, this means we will be unable to prove the intermediate value theorem as stated here (although versions with additional conditions, such as ivthinc 15500 for strictly monotonic functions, can be proved). The proof is via a function which we call the hover function and which is also described in Section 5.1 of [Bauer], p. 493. Consider any real number 𝑧. We want to show that 𝑧 ≤ 0 ∨ 0 ≤ 𝑧. Because of hovercncf 15503, hovera 15504, and hoverb 15505, we are able to apply the intermediate value theorem to get a value 𝑐 such that the hover function at 𝑐 equals 𝑧. By axltwlin 8340, 𝑐 < 1 or 0 < 𝑐, and that leads to 𝑧 ≤ 0 by hoverlt1 15506 or 0 ≤ 𝑧 by hovergt0 15507. (Contributed by Jim Kingdon and Mario Carneiro, 22-Jul-2025.)
⊢ (∀𝑓(𝑓 ∈ (ℝ–cn→ℝ) → ∀𝑎 ∈ ℝ ∀𝑏 ∈ ℝ ((𝑎 < 𝑏 ∧ (𝑓‘𝑎) < 0 ∧ 0 < (𝑓‘𝑏)) → ∃𝑥 ∈ ℝ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ∧ (𝑓‘𝑥) = 0))) → ∀𝑟 ∈ ℝ ∀𝑠 ∈ ℝ (𝑟 ≤ 𝑠 ∨ 𝑠 ≤ 𝑟))
10.2  Derivatives
10.2.1  Real and complex differentiation
10.2.1.1  Derivatives of functions of one complex or real variable
Syntax	climc 15511	The limit operator.
class limℂ
Syntax	cdv 15512	The derivative operator.
class D
Definition	df-limced 15513*	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.) (Revised by Jim Kingdon, 3-Jun-2023.)
⊢ limℂ = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)))})
Definition	df-dvap 15514*	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.) (Revised by Jim Kingdon, 25-Jun-2023.)
⊢ D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ ∪ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))
Theorem	limcrcl 15515	Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐶 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
Theorem	limccl 15516	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝐹 limℂ 𝐵) ⊆ ℂ
Theorem	ellimc3apf 15517*	Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 4-Nov-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ Ⅎ𝑧𝐹    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))
Theorem	ellimc3ap 15518*	Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) Use apartness. (Revised by Jim Kingdon, 3-Jun-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))
Theorem	limcdifap 15519*	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.) (Revised by Jim Kingdon, 3-Jun-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝑥 # 𝐵}) limℂ 𝐵))
Theorem	limcmpted 15520*	Express the limit operator for a function defined by a mapping, via epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ((𝑧 ∈ 𝐴 ↦ 𝐷) limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘(𝐷 − 𝐶)) < 𝑥))))
Theorem	limcimolemlt 15521*	Lemma for limcimo 15522. (Contributed by Jim Kingdon, 3-Jul-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾t 𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))    &   ⊢ (𝜑 → 𝐺 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))    ⇒   ⊢ (𝜑 → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))
Theorem	limcimo 15522*	Conditions which ensure there is at most one limit value of 𝐹 at 𝐵. (Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon, 8-Jul-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾t 𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐹 limℂ 𝐵))
Theorem	limcresi 15523	Any limit of 𝐹 is also a limit of the restriction of 𝐹. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ 𝐶) limℂ 𝐵)
Theorem	cnplimcim 15524	If a function is continuous at 𝐵, its limit at 𝐵 equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 14-Jun-2023.)
⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐽 = (𝐾 ↾t 𝐴)    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) → (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵))))
Theorem	cnplimclemle 15525	Lemma for cnplimccntop 15527. Satisfying the epsilon condition for continuity. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐽 = (𝐾 ↾t 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑍 # 𝐵 ∧ (abs‘(𝑍 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑍) − (𝐹‘𝐵))) < (𝐸 / 2))    &   ⊢ (𝜑 → (abs‘(𝑍 − 𝐵)) < 𝐷)    ⇒   ⊢ (𝜑 → (abs‘((𝐹‘𝑍) − (𝐹‘𝐵))) < 𝐸)
Theorem	cnplimclemr 15526	Lemma for cnplimccntop 15527. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐽 = (𝐾 ↾t 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))
Theorem	cnplimccntop 15527	A function is continuous at 𝐵 iff its limit at 𝐵 equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐽 = (𝐾 ↾t 𝐴)    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵))))
Theorem	cnlimcim 15528*	If 𝐹 is a continuous function, the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 16-Jun-2023.)
⊢ (𝐴 ⊆ ℂ → (𝐹 ∈ (𝐴–cn→ℂ) → (𝐹:𝐴⟶ℂ ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ (𝐹 limℂ 𝑥))))
Theorem	cnlimc 15529*	𝐹 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 15530	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 15531*	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	limccnpcntop 15532	If the limit of 𝐹 at 𝐵 is 𝐶 and 𝐺 is continuous at 𝐶, then the limit of 𝐺 ∘ 𝐹 at 𝐵 is 𝐺(𝐶). (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 18-Jun-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℂ)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐽 = (𝐾 ↾t 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐶))    ⇒   ⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝐺 ∘ 𝐹) limℂ 𝐵))
Theorem	limccnp2lem 15533*	Lemma for limccnp2cntop 15534. This is most of the result, expressed in epsilon-delta form, with a large number of hypotheses so that lengthy expressions do not need to be repeated. (Contributed by Jim Kingdon, 9-Nov-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑌 ⊆ ℂ)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐽 = ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌))    &   ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵))    &   ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑆) limℂ 𝐵))    &   ⊢ (𝜑 → 𝐻 ∈ ((𝐽 CnP 𝐾)‘⟨𝐶, 𝐷⟩))    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝐿 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝐿) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝐸))    &   ⊢ (𝜑 → 𝐹 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝐹) → (abs‘(𝑅 − 𝐶)) < 𝐿))    &   ⊢ (𝜑 → 𝐺 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝐺) → (abs‘(𝑆 − 𝐷)) < 𝐿))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑑) → (abs‘((𝑅𝐻𝑆) − (𝐶𝐻𝐷))) < 𝐸))
Theorem	limccnp2cntop 15534*	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.) (Revised by Jim Kingdon, 14-Nov-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑌 ⊆ ℂ)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐽 = ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌))    &   ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵))    &   ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑆) limℂ 𝐵))    &   ⊢ (𝜑 → 𝐻 ∈ ((𝐽 CnP 𝐾)‘⟨𝐶, 𝐷⟩))    ⇒   ⊢ (𝜑 → (𝐶𝐻𝐷) ∈ ((𝑥 ∈ 𝐴 ↦ (𝑅𝐻𝑆)) limℂ 𝐵))
Theorem	limccoap 15535*	Composition of two limits. This theorem is only usable in the case where 𝑥 # 𝑋 implies R(x) # 𝐶 so it is less general than might appear at first. (Contributed by Mario Carneiro, 29-Dec-2016.) (Revised by Jim Kingdon, 18-Dec-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑋}) → 𝑅 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤 # 𝐶})    &   ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤 # 𝐶}) → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑋} ↦ 𝑅) limℂ 𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ ((𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤 # 𝐶} ↦ 𝑆) limℂ 𝐶))    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑋} ↦ 𝑇) limℂ 𝑋))
Theorem	reldvg 15536	The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → Rel (𝑆 D 𝐹))
Theorem	dvlemap 15537*	Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    &   ⊢ (𝜑 → 𝐷 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑤 ∈ 𝐷 ∣ 𝑤 # 𝐵}) → (((𝐹‘𝐴) − (𝐹‘𝐵)) / (𝐴 − 𝐵)) ∈ ℂ)
Theorem	dvfvalap 15538*	Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
⊢ 𝑇 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → ((𝑆 D 𝐹) = ∪ 𝑥 ∈ ((int‘𝑇)‘𝐴)({𝑥} × ((𝑧 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑥} ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)) ∧ (𝑆 D 𝐹) ⊆ (((int‘𝑇)‘𝐴) × ℂ)))
Theorem	eldvap 15539*	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 Jim Kingdon, 27-Jun-2023.)
⊢ 𝑇 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐺 = (𝑧 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝐵} ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)))    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → (𝐵(𝑆 D 𝐹)𝐶 ↔ (𝐵 ∈ ((int‘𝑇)‘𝐴) ∧ 𝐶 ∈ (𝐺 limℂ 𝐵))))
Theorem	dvcl 15540	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	dvbssntrcntop 15541	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 Jim Kingdon, 27-Jun-2023.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ ((int‘𝐽)‘𝐴))
Theorem	dvbss 15542	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	dvbsssg 15543	The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Jim Kingdon, 28-Jun-2023.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → dom (𝑆 D 𝐹) ⊆ 𝑆)
Theorem	recnprss 15544	Both ℝ and ℂ are subsets of ℂ. (Contributed by Mario Carneiro, 10-Feb-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Theorem	dvfgg 15545	Explicitly write out the functionality condition on derivative for 𝑆 = ℝ and ℂ. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jun-2023.)
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)
Theorem	dvfpm 15546	The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.)
⊢ (𝐹 ∈ (ℂ ↑pm ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ)
Theorem	dvfcnpm 15547	The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.)
⊢ (𝐹 ∈ (ℂ ↑pm ℂ) → (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ)
Theorem	dvidlemap 15548*	Lemma for dvid 15552 and dvconst 15551. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (𝜑 → 𝐹:ℂ⟶ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵}))
Theorem	dvidrelem 15549*	Lemma for dvidre 15554 and dvconstre 15553. Analogue of dvidlemap 15548 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
⊢ (𝜑 → 𝐹:ℝ⟶ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ × {𝐵}))
Theorem	dvidsslem 15550*	Lemma for dvconstss 15555. Analogue of dvidlemap 15548 where 𝐹 is defined on an open subset of the real or complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝜑 → (𝑆 D 𝐹) = (𝑋 × {𝐵}))
Theorem	dvconst 15551	Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (𝐴 ∈ ℂ → (ℂ D (ℂ × {𝐴})) = (ℂ × {0}))
Theorem	dvid 15552	Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (ℂ D ( I ↾ ℂ)) = (ℂ × {1})
Theorem	dvconstre 15553	Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.)
⊢ (𝐴 ∈ ℂ → (ℝ D (ℝ × {𝐴})) = (ℝ × {0}))
Theorem	dvidre 15554	Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)
⊢ (ℝ D ( I ↾ ℝ)) = (ℝ × {1})
Theorem	dvconstss 15555	Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑋 × {𝐴})) = (𝑋 × {0}))
Theorem	dvcnp2cntop 15556	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 𝐴)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))
Theorem	dvcn 15557	A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ dom (𝑆 D 𝐹) = 𝐴) → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	dvaddxxbr 15558	The sum rule for derivatives at a point. That is, if the derivative of 𝐹 at 𝐶 is 𝐾 and the derivative of 𝐺 at 𝐶 is 𝐿, then the derivative of the pointwise sum of those two functions at 𝐶 is 𝐾 + 𝐿. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)    &   ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 + 𝐺))(𝐾 + 𝐿))
Theorem	dvmulxxbr 15559	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 15561. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)    &   ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))
Theorem	dvaddxx 15560	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 15558. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 + 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘𝐶) + ((𝑆 D 𝐺)‘𝐶)))
Theorem	dvmulxx 15561	The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 15559. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 · 𝐺))‘𝐶) = ((((𝑆 D 𝐹)‘𝐶) · (𝐺‘𝐶)) + (((𝑆 D 𝐺)‘𝐶) · (𝐹‘𝐶))))
Theorem	dviaddf 15562	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 (𝐹 ∘𝑓 + 𝐺)) = ((𝑆 D 𝐹) ∘𝑓 + (𝑆 D 𝐺)))
Theorem	dvimulf 15563	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 (𝐹 ∘𝑓 · 𝐺)) = (((𝑆 D 𝐹) ∘𝑓 · 𝐺) ∘𝑓 + ((𝑆 D 𝐺) ∘𝑓 · 𝐹)))
Theorem	dvcoapbr 15564*	The chain rule for derivatives at a point. The 𝑢 # 𝐶 → (𝐺‘𝑢) # (𝐺‘𝐶) hypothesis constrains what functions work for 𝐺. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 21-Dec-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶𝑋)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑇)    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝑌 (𝑢 # 𝐶 → (𝐺‘𝑢) # (𝐺‘𝐶)))    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑇 ⊆ ℂ)    &   ⊢ (𝜑 → (𝐺‘𝐶)(𝑆 D 𝐹)𝐾)    &   ⊢ (𝜑 → 𝐶(𝑇 D 𝐺)𝐿)    &   ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ (𝜑 → 𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿))
Theorem	dvcjbr 15565	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 15566. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ dom (ℝ D 𝐹))    ⇒   ⊢ (𝜑 → 𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶)))
Theorem	dvcj 15566	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 15565. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → (ℝ D (∗ ∘ 𝐹)) = (∗ ∘ (ℝ D 𝐹)))
Theorem	dvfre 15567	The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
Theorem	dvexp 15568*	Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
Theorem	dvexp2 15569*	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	dvrecap 15570*	Derivative of the reciprocal function. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐴 ∈ ℂ → (ℂ D (𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 0} ↦ (𝐴 / 𝑥))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 0} ↦ -(𝐴 / (𝑥↑2))))
Theorem	dvmptidcn 15571	Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.)
⊢ (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1)
Theorem	dvmptccn 15572*	Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 0))
Theorem	dvmptid 15573*	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 15574*	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	dvmptclx 15575*	Closure lemma for dvmptmulx 15577 and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ)
Theorem	dvmptaddx 15576*	Function-builder for derivative, addition rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 + 𝐷)))
Theorem	dvmptmulx 15577*	Function-builder for derivative, product rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐶))) = (𝑥 ∈ 𝑋 ↦ ((𝐵 · 𝐶) + (𝐷 · 𝐴))))
Theorem	dvmptcmulcn 15578*	Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝐶 · 𝐴))) = (𝑥 ∈ ℂ ↦ (𝐶 · 𝐵)))
Theorem	dvmptnegcn 15579*	Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))    ⇒   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ -𝐴)) = (𝑥 ∈ ℂ ↦ -𝐵))
Theorem	dvmptsubcn 15580*	Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐶)) = (𝑥 ∈ ℂ ↦ 𝐷))    ⇒   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 − 𝐶))) = (𝑥 ∈ ℂ ↦ (𝐵 − 𝐷)))
Theorem	dvmptcjx 15581*	Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (∗‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (∗‘𝐵)))
Theorem	dvmptfsum 15582*	Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵))
Theorem	dveflem 15583	Derivative of the exponential function at 0. The key step in the proof is eftlub 12372, 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 15584	Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
⊢ (ℂ D exp) = exp
PART 11  BASIC REAL AND COMPLEX FUNCTIONS
11.1  Polynomials
11.1.1  Elementary properties of complex polynomials
Syntax	cply 15585	Extend class notation to include the set of complex polynomials.
class Poly
Syntax	cidp 15586	Extend class notation to include the identity polynomial.
class Xp
Definition	df-ply 15587*	Define the set of polynomials on the complex numbers with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ Poly = (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
Definition	df-idp 15588	Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ Xp = ( I ↾ ℂ)
Theorem	plyval 15589*	Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝑆 ⊆ ℂ → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
Theorem	plybss 15590	Reverse closure of the parameter 𝑆 of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ)
Theorem	elply 15591*	Definition of a polynomial with coefficients in 𝑆. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚 ℕ0)𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
Theorem	elply2 15592*	The coefficient function can be assumed to have zeroes outside 0...𝑛. (Contributed by Mario Carneiro, 20-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))
Theorem	plyun0 15593	The set of polynomials is unaffected by the addition of zero. (This is built into the definition because all higher powers of a polynomial are effectively zero, so we require that the coefficient field contain zero to simplify some of our closure theorems.) (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (Poly‘(𝑆 ∪ {0})) = (Poly‘𝑆)
Theorem	plyf 15594	A polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
Theorem	plyss 15595	The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇))
Theorem	plyssc 15596	Every polynomial ring is contained in the ring of polynomials over ℂ. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (Poly‘𝑆) ⊆ (Poly‘ℂ)
Theorem	elplyr 15597*	Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
Theorem	elplyd 15598*	Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
Theorem	ply1termlem 15599*	Lemma for ply1term 15600. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))))
Theorem	ply1term 15600*	A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆))