P. 140 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13901-14000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ivthinclemloc 13901*	Lemma for ivthinc 13903. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑅)))
Theorem	ivthinclemex 13902*	Lemma for ivthinc 13903. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   ⊢ (𝜑 → ∃!𝑧 ∈ (𝐴(,)𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑧 ∧ ∀𝑟 ∈ 𝑅 𝑧 < 𝑟))
Theorem	ivthinc 13903*	The intermediate value theorem, increasing case, for a strictly monotonic function. Theorem 5.5 of [Bauer], p. 494. This is Metamath 100 proof #79. (Contributed by Jim Kingdon, 5-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivthdec 13904*	The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑦) < (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
9.1  Derivatives
9.1.1  Real and complex differentiation
9.1.1.1  Derivatives of functions of one complex or real variable
Syntax	climc 13905	The limit operator.
class limℂ
Syntax	cdv 13906	The derivative operator.
class D
Definition	df-limced 13907*	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 13908*	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 13909	Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐶 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
Theorem	limccl 13910	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝐹 limℂ 𝐵) ⊆ ℂ
Theorem	ellimc3apf 13911*	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 13912*	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 13913*	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 13914*	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 13915*	Lemma for limcimo 13916. (Contributed by Jim Kingdon, 3-Jul-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾t 𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))    &   ⊢ (𝜑 → 𝐺 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))    ⇒   ⊢ (𝜑 → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))
Theorem	limcimo 13916*	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 13917	Any limit of 𝐹 is also a limit of the restriction of 𝐹. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ 𝐶) limℂ 𝐵)
Theorem	cnplimcim 13918	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 13919	Lemma for cnplimccntop 13921. 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 13920	Lemma for cnplimccntop 13921. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐽 = (𝐾 ↾t 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))
Theorem	cnplimccntop 13921	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 13922*	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 13923*	𝐹 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 13924	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 13925*	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 13926	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 13927*	Lemma for limccnp2cntop 13928. 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 13928*	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 13929*	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 13930	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 13931*	Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    &   ⊢ (𝜑 → 𝐷 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑤 ∈ 𝐷 ∣ 𝑤 # 𝐵}) → (((𝐹‘𝐴) − (𝐹‘𝐵)) / (𝐴 − 𝐵)) ∈ ℂ)
Theorem	dvfvalap 13932*	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 13933*	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 13934	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 13935	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 13936	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 13937	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 13938	Both ℝ and ℂ are subsets of ℂ. (Contributed by Mario Carneiro, 10-Feb-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Theorem	dvfgg 13939	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 13940	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 13941	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 13942*	Lemma for dvid 13944 and dvconst 13943. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (𝜑 → 𝐹:ℂ⟶ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵}))
Theorem	dvconst 13943	Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (𝐴 ∈ ℂ → (ℂ D (ℂ × {𝐴})) = (ℂ × {0}))
Theorem	dvid 13944	Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (ℂ D ( I ↾ ℂ)) = (ℂ × {1})
Theorem	dvcnp2cntop 13945	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 13946	A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ dom (𝑆 D 𝐹) = 𝐴) → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	dvaddxxbr 13947	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 13948	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 13950. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)    &   ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))
Theorem	dvaddxx 13949	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 13947. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 + 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘𝐶) + ((𝑆 D 𝐺)‘𝐶)))
Theorem	dvmulxx 13950	The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 13948. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 · 𝐺))‘𝐶) = ((((𝑆 D 𝐹)‘𝐶) · (𝐺‘𝐶)) + (((𝑆 D 𝐺)‘𝐶) · (𝐹‘𝐶))))
Theorem	dviaddf 13951	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 13952	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 13953*	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 13954	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 13955. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ dom (ℝ D 𝐹))    ⇒   ⊢ (𝜑 → 𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶)))
Theorem	dvcj 13955	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 13954. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → (ℝ D (∗ ∘ 𝐹)) = (∗ ∘ (ℝ D 𝐹)))
Theorem	dvfre 13956	The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
Theorem	dvexp 13957*	Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
Theorem	dvexp2 13958*	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 13959*	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 13960	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 13961*	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	dvmptclx 13962*	Closure lemma for dvmptmulx 13964 and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ)
Theorem	dvmptaddx 13963*	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 13964*	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 13965*	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 13966*	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 13967*	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 13968*	Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (∗‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (∗‘𝐵)))
Theorem	dveflem 13969	Derivative of the exponential function at 0. The key step in the proof is eftlub 11689, 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 13970	Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
⊢ (ℂ D exp) = exp
PART 10  BASIC REAL AND COMPLEX FUNCTIONS
10.1  Basic trigonometry
10.1.1  The exponential, sine, and cosine functions (cont.)
Theorem	efcn 13971	The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ exp ∈ (ℂ–cn→ℂ)
Theorem	sincn 13972	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ sin ∈ (ℂ–cn→ℂ)
Theorem	coscn 13973	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ cos ∈ (ℂ–cn→ℂ)
Theorem	reeff1olem 13974*	Lemma for reeff1o 13976. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈)
Theorem	reeff1oleme 13975*	Lemma for reeff1o 13976. (Contributed by Jim Kingdon, 15-May-2024.)
⊢ (𝑈 ∈ (0(,)e) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈)
Theorem	reeff1o 13976	The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (exp ↾ ℝ):ℝ–1-1-onto→ℝ+
Theorem	efltlemlt 13977	Lemma for eflt 13978. The converse of efltim 11697 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (exp‘𝐴) < (exp‘𝐵))    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < 𝐷 → (abs‘((exp‘𝐴) − (exp‘𝐵))) < ((exp‘𝐵) − (exp‘𝐴))))    ⇒   ⊢ (𝜑 → 𝐴 < 𝐵)
Theorem	eflt 13978	The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 21-May-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (exp‘𝐴) < (exp‘𝐵)))
Theorem	efle 13979	The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (exp‘𝐴) ≤ (exp‘𝐵)))
Theorem	reefiso 13980	The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) (Revised by Mario Carneiro, 11-Mar-2014.)
⊢ (exp ↾ ℝ) Isom < , < (ℝ, ℝ+)
Theorem	reapef 13981	Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 # 𝐵 ↔ (exp‘𝐴) # (exp‘𝐵)))
10.1.2  Properties of pi = 3.14159...
Theorem	pilem1 13982	Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0))
Theorem	cosz12 13983	Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.)
⊢ ∃𝑝 ∈ (1(,)2)(cos‘𝑝) = 0
Theorem	sin0pilem1 13984*	Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
⊢ ∃𝑝 ∈ (1(,)2)((cos‘𝑝) = 0 ∧ ∀𝑥 ∈ (𝑝(,)(2 · 𝑝))0 < (sin‘𝑥))
Theorem	sin0pilem2 13985*	Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
⊢ ∃𝑞 ∈ (2(,)4)((sin‘𝑞) = 0 ∧ ∀𝑥 ∈ (0(,)𝑞)0 < (sin‘𝑥))
Theorem	pilem3 13986	Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.)
⊢ (π ∈ (2(,)4) ∧ (sin‘π) = 0)
Theorem	pigt2lt4 13987	π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ (2 < π ∧ π < 4)
Theorem	sinpi 13988	The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘π) = 0
Theorem	pire 13989	π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ π ∈ ℝ
Theorem	picn 13990	π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ π ∈ ℂ
Theorem	pipos 13991	π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ 0 < π
Theorem	pirp 13992	π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ π ∈ ℝ+
Theorem	negpicn 13993	-π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -π ∈ ℂ
Theorem	sinhalfpilem 13994	Lemma for sinhalfpi 13999 and coshalfpi 14000. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0)
Theorem	halfpire 13995	π / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
⊢ (π / 2) ∈ ℝ
Theorem	neghalfpire 13996	-π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ
Theorem	neghalfpirx 13997	-π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ*
Theorem	pidiv2halves 13998	Adding π / 2 to itself gives π. See 2halves 9142. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ((π / 2) + (π / 2)) = π
Theorem	sinhalfpi 13999	The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(π / 2)) = 1
Theorem	coshalfpi 14000	The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘(π / 2)) = 0