P. 154 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15301-15400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	negfcncf 15301*	The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -(𝐹‘𝑥))    ⇒   ⊢ (𝐹 ∈ (𝐴–cn→ℂ) → 𝐺 ∈ (𝐴–cn→ℂ))
Theorem	mulcncflem 15302*	Lemma for mulcncf 15303. (Contributed by Jim Kingdon, 29-May-2023.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑆 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝑋 ((abs‘(𝑢 − 𝑉)) < 𝑆 → (abs‘(((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑢) − ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑉))) < 𝐹))    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝑋 ((abs‘(𝑢 − 𝑉)) < 𝑇 → (abs‘(((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑢) − ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑉))) < 𝐺))    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝑋 (((abs‘(⦋𝑢 / 𝑥⦌𝐴 − ⦋𝑉 / 𝑥⦌𝐴)) < 𝐹 ∧ (abs‘(⦋𝑢 / 𝑥⦌𝐵 − ⦋𝑉 / 𝑥⦌𝐵)) < 𝐺) → (abs‘((⦋𝑢 / 𝑥⦌𝐴 · ⦋𝑢 / 𝑥⦌𝐵) − (⦋𝑉 / 𝑥⦌𝐴 · ⦋𝑉 / 𝑥⦌𝐵))) < 𝐸))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ((abs‘(𝑢 − 𝑉)) < 𝑑 → (abs‘(((𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵))‘𝑢) − ((𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵))‘𝑉))) < 𝐸))
Theorem	mulcncf 15303*	The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	expcncf 15304*	The power function on complex numbers, for fixed exponent N, is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ))
Theorem	cnrehmeocntop 15305*	The canonical bijection from (ℝ × ℝ) to ℂ described in cnref1o 9863 is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if (ℝ × ℝ) is metrized with the l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾)
Theorem	cnopnap 15306*	The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.)
⊢ (𝐴 ∈ ℂ → {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ∈ (MetOpen‘(abs ∘ − )))
PART 10  BASIC REAL AND COMPLEX ANALYSIS
10.1  Continuity
Theorem	addcncf 15307*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	subcncf 15308*	The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 − 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	divcncfap 15309*	The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→{𝑦 ∈ ℂ ∣ 𝑦 # 0}))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	maxcncf 15310*	The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℝ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℝ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ sup({𝐴, 𝐵}, ℝ, < )) ∈ (𝑋–cn→ℝ))
Theorem	mincncf 15311*	The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℝ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℝ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ inf({𝐴, 𝐵}, ℝ, < )) ∈ (𝑋–cn→ℝ))
10.1.1  Dedekind cuts
Theorem	dedekindeulemuub 15312*	Lemma for dedekindeu 15318. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐿 𝑧 < 𝐴)
Theorem	dedekindeulemub 15313*	Lemma for dedekindeu 15318. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐿 𝑦 < 𝑥)
Theorem	dedekindeulemloc 15314*	Lemma for dedekindeu 15318. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐿 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐿 𝑧 < 𝑦)))
Theorem	dedekindeulemlub 15315*	Lemma for dedekindeu 15318. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)))
Theorem	dedekindeulemlu 15316*	Lemma for dedekindeu 15318. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
Theorem	dedekindeulemeu 15317*	Lemma for dedekindeu 15318. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐴 ∧ ∀𝑟 ∈ 𝑈 𝐴 < 𝑟))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐵 ∧ ∀𝑟 ∈ 𝑈 𝐵 < 𝑟))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ⊥)
Theorem	dedekindeu 15318*	A Dedekind cut identifies a unique real number. Similar to df-inp 7669 except that the the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 5-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
Theorem	suplociccreex 15319*	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8235 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶))    &   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ (𝐵[,]𝐶)(𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	suplociccex 15320*	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8235 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶))    &   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ (𝐵[,]𝐶)(𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐵[,]𝐶)(∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐵[,]𝐶)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	dedekindicclemuub 15321*	Lemma for dedekindicc 15328. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 15-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐿 𝑧 < 𝐶)
Theorem	dedekindicclemub 15322*	Lemma for dedekindicc 15328. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ 𝐿 𝑦 < 𝑥)
Theorem	dedekindicclemloc 15323*	Lemma for dedekindicc 15328. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (∃𝑧 ∈ 𝐿 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐿 𝑧 < 𝑦)))
Theorem	dedekindicclemlub 15324*	Lemma for dedekindicc 15328. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)))
Theorem	dedekindicclemlu 15325*	Lemma for dedekindicc 15328. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
Theorem	dedekindicclemeu 15326*	Lemma for dedekindicc 15328. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐶 ∧ ∀𝑟 ∈ 𝑈 𝐶 < 𝑟))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐷 ∧ ∀𝑟 ∈ 𝑈 𝐷 < 𝑟))    &   ⊢ (𝜑 → 𝐶 < 𝐷)    ⇒   ⊢ (𝜑 → ⊥)
Theorem	dedekindicclemicc 15327*	Lemma for dedekindicc 15328. Same as dedekindicc 15328, except that we merely show 𝑥 to be an element of (𝐴[,]𝐵). Later we will strengthen that to (𝐴(,)𝐵). (Contributed by Jim Kingdon, 5-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
Theorem	dedekindicc 15328*	A Dedekind cut identifies a unique real number. Similar to df-inp 7669 except that the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 19-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ (𝐴(,)𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
10.1.2  Intermediate value theorem
Theorem	ivthinclemlm 15329*	Lemma for ivthinc 15338. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
Theorem	ivthinclemum 15330*	Lemma for ivthinc 15338. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑅)
Theorem	ivthinclemlopn 15331*	Lemma for ivthinc 15338. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    &   ⊢ (𝜑 → 𝑄 ∈ 𝐿)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ 𝐿 𝑄 < 𝑟)
Theorem	ivthinclemlr 15332*	Lemma for ivthinc 15338. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
Theorem	ivthinclemuopn 15333*	Lemma for ivthinc 15338. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    &   ⊢ (𝜑 → 𝑆 ∈ 𝑅)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝑅 𝑞 < 𝑆)
Theorem	ivthinclemur 15334*	Lemma for ivthinc 15338. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑅 ↔ ∃𝑞 ∈ 𝑅 𝑞 < 𝑟))
Theorem	ivthinclemdisj 15335*	Lemma for ivthinc 15338. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   ⊢ (𝜑 → (𝐿 ∩ 𝑅) = ∅)
Theorem	ivthinclemloc 15336*	Lemma for ivthinc 15338. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑅)))
Theorem	ivthinclemex 15337*	Lemma for ivthinc 15338. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   ⊢ (𝜑 → ∃!𝑧 ∈ (𝐴(,)𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑧 ∧ ∀𝑟 ∈ 𝑅 𝑧 < 𝑟))
Theorem	ivthinc 15338*	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 15339*	The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴)))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑦) < (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivthreinc 15340*	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 15338). 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 15341	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 15342*	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 15343*	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 15344*	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 15345*	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 15346*	Lemma for ivthdich 15348. 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 15347*	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 15348*	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 15338 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 15341, hovera 15342, and hoverb 15343, we are able to apply the intermediate value theorem to get a value 𝑐 such that the hover function at 𝑐 equals 𝑧. By axltwlin 8230, 𝑐 < 1 or 0 < 𝑐, and that leads to 𝑧 ≤ 0 by hoverlt1 15344 or 0 ≤ 𝑧 by hovergt0 15345. (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 15349	The limit operator.
class limℂ
Syntax	cdv 15350	The derivative operator.
class D
Definition	df-limced 15351*	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 15352*	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 15353	Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐶 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
Theorem	limccl 15354	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝐹 limℂ 𝐵) ⊆ ℂ
Theorem	ellimc3apf 15355*	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 15356*	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 15357*	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 15358*	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 15359*	Lemma for limcimo 15360. (Contributed by Jim Kingdon, 3-Jul-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾t 𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))    &   ⊢ (𝜑 → 𝐺 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))    ⇒   ⊢ (𝜑 → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))
Theorem	limcimo 15360*	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 15361	Any limit of 𝐹 is also a limit of the restriction of 𝐹. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ 𝐶) limℂ 𝐵)
Theorem	cnplimcim 15362	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 15363	Lemma for cnplimccntop 15365. 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 15364	Lemma for cnplimccntop 15365. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐽 = (𝐾 ↾t 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))
Theorem	cnplimccntop 15365	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 15366*	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 15367*	𝐹 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 15368	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 15369*	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 15370	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 15371*	Lemma for limccnp2cntop 15372. 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 15372*	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 15373*	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 15374	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 15375*	Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    &   ⊢ (𝜑 → 𝐷 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑤 ∈ 𝐷 ∣ 𝑤 # 𝐵}) → (((𝐹‘𝐴) − (𝐹‘𝐵)) / (𝐴 − 𝐵)) ∈ ℂ)
Theorem	dvfvalap 15376*	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 15377*	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 15378	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 15379	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 15380	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 15381	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 15382	Both ℝ and ℂ are subsets of ℂ. (Contributed by Mario Carneiro, 10-Feb-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Theorem	dvfgg 15383	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 15384	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 15385	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 15386*	Lemma for dvid 15390 and dvconst 15389. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (𝜑 → 𝐹:ℂ⟶ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵}))
Theorem	dvidrelem 15387*	Lemma for dvidre 15392 and dvconstre 15391. Analogue of dvidlemap 15386 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
⊢ (𝜑 → 𝐹:ℝ⟶ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ × {𝐵}))
Theorem	dvidsslem 15388*	Lemma for dvconstss 15393. Analogue of dvidlemap 15386 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 15389	Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (𝐴 ∈ ℂ → (ℂ D (ℂ × {𝐴})) = (ℂ × {0}))
Theorem	dvid 15390	Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (ℂ D ( I ↾ ℂ)) = (ℂ × {1})
Theorem	dvconstre 15391	Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.)
⊢ (𝐴 ∈ ℂ → (ℝ D (ℝ × {𝐴})) = (ℝ × {0}))
Theorem	dvidre 15392	Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)
⊢ (ℝ D ( I ↾ ℝ)) = (ℝ × {1})
Theorem	dvconstss 15393	Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑋 × {𝐴})) = (𝑋 × {0}))
Theorem	dvcnp2cntop 15394	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 15395	A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ dom (𝑆 D 𝐹) = 𝐴) → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	dvaddxxbr 15396	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 15397	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 15399. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)    &   ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))
Theorem	dvaddxx 15398	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 15396. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 + 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘𝐶) + ((𝑆 D 𝐺)‘𝐶)))
Theorem	dvmulxx 15399	The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 15397. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 · 𝐺))‘𝐶) = ((((𝑆 D 𝐹)‘𝐶) · (𝐺‘𝐶)) + (((𝑆 D 𝐺)‘𝐶) · (𝐹‘𝐶))))
Theorem	dviaddf 15400	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 𝐺)))