Home Intuitionistic Logic ExplorerTheorem List (p. 129 of 135) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 12801-12900   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremexpcncf 12801* The power function on complex numbers, for fixed exponent N, is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
(𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥𝑁)) ∈ (ℂ–cn→ℂ))

Theoremcnrehmeocntop 12802* The canonical bijection from (ℝ × ℝ) to described in cnref1o 9470 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𝐾)

Theoremcnopnap 12803* The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.)
(𝐴 ∈ ℂ → {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ∈ (MetOpen‘(abs ∘ − )))

PART 8  BASIC REAL AND COMPLEX ANALYSIS

8.0.1  Dedekind cuts

Theoremdedekindeulemuub 12804* Lemma for dedekindeu 12810. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
(𝜑𝐿 ⊆ ℝ)    &   (𝜑𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))    &   (𝜑𝐴𝑈)       (𝜑 → ∀𝑧𝐿 𝑧 < 𝐴)

Theoremdedekindeulemub 12805* Lemma for dedekindeu 12810. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
(𝜑𝐿 ⊆ ℝ)    &   (𝜑𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))       (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐿 𝑦 < 𝑥)

Theoremdedekindeulemloc 12806* Lemma for dedekindeu 12810. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.)
(𝜑𝐿 ⊆ ℝ)    &   (𝜑𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))       (𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐿 𝑥 < 𝑧 ∨ ∀𝑧𝐿 𝑧 < 𝑦)))

Theoremdedekindeulemlub 12807* Lemma for dedekindeu 12810. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
(𝜑𝐿 ⊆ ℝ)    &   (𝜑𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))       (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)))

Theoremdedekindeulemlu 12808* Lemma for dedekindeu 12810. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
(𝜑𝐿 ⊆ ℝ)    &   (𝜑𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))       (𝜑 → ∃𝑥 ∈ ℝ (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))

Theoremdedekindeulemeu 12809* Lemma for dedekindeu 12810. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.)
(𝜑𝐿 ⊆ ℝ)    &   (𝜑𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → (∀𝑞𝐿 𝑞 < 𝐴 ∧ ∀𝑟𝑈 𝐴 < 𝑟))    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → (∀𝑞𝐿 𝑞 < 𝐵 ∧ ∀𝑟𝑈 𝐵 < 𝑟))    &   (𝜑𝐴 < 𝐵)       (𝜑 → ⊥)

Theoremdedekindeu 12810* A Dedekind cut identifies a unique real number. Similar to df-inp 7299 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.)
(𝜑𝐿 ⊆ ℝ)    &   (𝜑𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))       (𝜑 → ∃!𝑥 ∈ ℝ (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))

Theoremsuplociccreex 12811* An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7862 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
(𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐵 < 𝐶)    &   (𝜑𝐴 ⊆ (𝐵[,]𝐶))    &   (𝜑 → ∃𝑥 𝑥𝐴)    &   (𝜑 → ∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ (𝐵[,]𝐶)(𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦)))       (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))

Theoremsuplociccex 12812* An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7862 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
(𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐵 < 𝐶)    &   (𝜑𝐴 ⊆ (𝐵[,]𝐶))    &   (𝜑 → ∃𝑥 𝑥𝐴)    &   (𝜑 → ∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ (𝐵[,]𝐶)(𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦)))       (𝜑 → ∃𝑥 ∈ (𝐵[,]𝐶)(∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐵[,]𝐶)(𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))

Theoremdedekindicclemuub 12813* Lemma for dedekindicc 12820. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))    &   (𝜑𝐶𝑈)       (𝜑 → ∀𝑧𝐿 𝑧 < 𝐶)

Theoremdedekindicclemub 12814* Lemma for dedekindicc 12820. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))       (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦𝐿 𝑦 < 𝑥)

Theoremdedekindicclemloc 12815* Lemma for dedekindicc 12820. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))       (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (∃𝑧𝐿 𝑥 < 𝑧 ∨ ∀𝑧𝐿 𝑧 < 𝑦)))

Theoremdedekindicclemlub 12816* Lemma for dedekindicc 12820. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))    &   (𝜑𝐴 < 𝐵)       (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)))

Theoremdedekindicclemlu 12817* Lemma for dedekindicc 12820. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))    &   (𝜑𝐴 < 𝐵)       (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))

Theoremdedekindicclemeu 12818* Lemma for dedekindicc 12820. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐶 ∈ (𝐴[,]𝐵))    &   (𝜑 → (∀𝑞𝐿 𝑞 < 𝐶 ∧ ∀𝑟𝑈 𝐶 < 𝑟))    &   (𝜑𝐷 ∈ (𝐴[,]𝐵))    &   (𝜑 → (∀𝑞𝐿 𝑞 < 𝐷 ∧ ∀𝑟𝑈 𝐷 < 𝑟))    &   (𝜑𝐶 < 𝐷)       (𝜑 → ⊥)

Theoremdedekindicclemicc 12819* Lemma for dedekindicc 12820. Same as dedekindicc 12820, except that we merely show 𝑥 to be an element of (𝐴[,]𝐵). Later we will strengthen that to (𝐴(,)𝐵). (Contributed by Jim Kingdon, 5-Jan-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))    &   (𝜑𝐴 < 𝐵)       (𝜑 → ∃!𝑥 ∈ (𝐴[,]𝐵)(∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))

Theoremdedekindicc 12820* A Dedekind cut identifies a unique real number. Similar to df-inp 7299 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.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))    &   (𝜑𝐴 < 𝐵)       (𝜑 → ∃!𝑥 ∈ (𝐴(,)𝐵)(∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))

8.0.2  Intermediate value theorem

Theoremivthinclemlm 12821* Lemma for ivthinc 12830. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑𝐹 ∈ (𝐷cn→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}       (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞𝐿)

Theoremivthinclemum 12822* Lemma for ivthinc 12830. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑𝐹 ∈ (𝐷cn→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}       (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟𝑅)

Theoremivthinclemlopn 12823* Lemma for ivthinc 12830. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑𝐹 ∈ (𝐷cn→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}    &   (𝜑𝑄𝐿)       (𝜑 → ∃𝑟𝐿 𝑄 < 𝑟)

Theoremivthinclemlr 12824* Lemma for ivthinc 12830. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑𝐹 ∈ (𝐷cn→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}       (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))

Theoremivthinclemuopn 12825* Lemma for ivthinc 12830. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑𝐹 ∈ (𝐷cn→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}    &   (𝜑𝑆𝑅)       (𝜑 → ∃𝑞𝑅 𝑞 < 𝑆)

Theoremivthinclemur 12826* Lemma for ivthinc 12830. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑𝐹 ∈ (𝐷cn→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}       (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟𝑅 ↔ ∃𝑞𝑅 𝑞 < 𝑟))

Theoremivthinclemdisj 12827* Lemma for ivthinc 12830. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑𝐹 ∈ (𝐷cn→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}       (𝜑 → (𝐿𝑅) = ∅)

Theoremivthinclemloc 12828* Lemma for ivthinc 12830. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑𝐹 ∈ (𝐷cn→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}       (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑅)))

Theoremivthinclemex 12829* Lemma for ivthinc 12830. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑𝐹 ∈ (𝐷cn→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}       (𝜑 → ∃!𝑧 ∈ (𝐴(,)𝐵)(∀𝑞𝐿 𝑞 < 𝑧 ∧ ∀𝑟𝑅 𝑧 < 𝑟))

Theoremivthinc 12830* 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→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))       (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹𝑐) = 𝑈)

Theoremivthdec 12831* The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑𝐹 ∈ (𝐷cn→ℂ))    &   ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹𝐵) < 𝑈𝑈 < (𝐹𝐴)))    &   (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑦) < (𝐹𝑥))       (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹𝑐) = 𝑈)

8.1  Derivatives

8.1.1  Real and complex differentiation

8.1.1.1  Derivatives of functions of one complex or real variable

Syntaxclimc 12832 The limit operator.
class lim

Syntaxcdv 12833 The derivative operator.
class D

Definitiondf-limced 12834* 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‘((𝑓𝑧) − 𝑦)) < 𝑒)))})

Definitiondf-dvap 12835* 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 𝑥)))

Theoremlimcrcl 12836 Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.)
(𝐶 ∈ (𝐹 lim 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))

Theoremlimccl 12837 Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
(𝐹 lim 𝐵) ⊆ ℂ

Theoremellimc3apf 12838* 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‘((𝐹𝑧) − 𝐶)) < 𝑥))))

Theoremellimc3ap 12839* 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‘((𝐹𝑧) − 𝐶)) < 𝑥))))

Theoremlimcdifap 12840* 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 𝐵))

Theoremlimcmpted 12841* Express the limit operator for a function defined by a mapping, via epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.)
(𝜑𝐴 ⊆ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   ((𝜑𝑧𝐴) → 𝐷 ∈ ℂ)       (𝜑 → (𝐶 ∈ ((𝑧𝐴𝐷) lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘(𝐷𝐶)) < 𝑥))))

Theoremlimcimolemlt 12842* Lemma for limcimo 12843. (Contributed by Jim Kingdon, 3-Jul-2023.)
(𝜑𝐹:𝐴⟶ℂ)    &   (𝜑𝐴 ⊆ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐵𝐶)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶 ∈ (𝐾t 𝑆))    &   (𝜑𝑆 ∈ {ℝ, ℂ})    &   (𝜑 → {𝑞𝐶𝑞 # 𝐵} ⊆ 𝐴)    &   𝐾 = (MetOpen‘(abs ∘ − ))    &   (𝜑𝐷 ∈ ℝ+)    &   (𝜑𝑋 ∈ (𝐹 lim 𝐵))    &   (𝜑𝑌 ∈ (𝐹 lim 𝐵))    &   (𝜑 → ∀𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝐷) → (abs‘((𝐹𝑧) − 𝑋)) < ((abs‘(𝑋𝑌)) / 2)))    &   (𝜑𝐺 ∈ ℝ+)    &   (𝜑 → ∀𝑤𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤𝐵)) < 𝐺) → (abs‘((𝐹𝑤) − 𝑌)) < ((abs‘(𝑋𝑌)) / 2)))       (𝜑 → (abs‘(𝑋𝑌)) < (abs‘(𝑋𝑌)))

Theoremlimcimo 12843* 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 𝐵))

Theoremlimcresi 12844 Any limit of 𝐹 is also a limit of the restriction of 𝐹. (Contributed by Mario Carneiro, 28-Dec-2016.)
(𝐹 lim 𝐵) ⊆ ((𝐹𝐶) lim 𝐵)

Theoremcnplimcim 12845 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 𝐵))))

Theoremcnplimclemle 12846 Lemma for cnplimccntop 12848. 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‘((𝐹𝑍) − (𝐹𝐵))) < 𝐸)

Theoremcnplimclemr 12847 Lemma for cnplimccntop 12848. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
𝐾 = (MetOpen‘(abs ∘ − ))    &   𝐽 = (𝐾t 𝐴)    &   (𝜑𝐴 ⊆ ℂ)    &   (𝜑𝐹:𝐴⟶ℂ)    &   (𝜑𝐵𝐴)    &   (𝜑 → (𝐹𝐵) ∈ (𝐹 lim 𝐵))       (𝜑𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))

Theoremcnplimccntop 12848 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 𝐵))))

Theoremcnlimcim 12849* 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 𝑥))))

Theoremcnlimc 12850* 𝐹 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 𝑥))))

Theoremcnlimci 12851 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 𝐵))

Theoremcnmptlimc 12852* 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 𝐵))

Theoremlimccnpcntop 12853 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 𝐵))

Theoremlimccnp2lem 12854* Lemma for limccnp2cntop 12855. 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‘((𝑅𝐻𝑆) − (𝐶𝐻𝐷))) < 𝐸))

Theoremlimccnp2cntop 12855* 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 𝐵))

Theoremlimccoap 12856* 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 𝑋))

Theoremreldvg 12857 The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.)
((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → Rel (𝑆 D 𝐹))

Theoremdvlemap 12858* Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
(𝜑𝐹:𝐷⟶ℂ)    &   (𝜑𝐷 ⊆ ℂ)    &   (𝜑𝐵𝐷)       ((𝜑𝐴 ∈ {𝑤𝐷𝑤 # 𝐵}) → (((𝐹𝐴) − (𝐹𝐵)) / (𝐴𝐵)) ∈ ℂ)

Theoremdvfvalap 12859* 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‘𝑇)‘𝐴) × ℂ)))

Theoremeldvap 12860* 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 𝐵))))

Theoremdvcl 12861 The derivative function takes values in the complex numbers. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
(𝜑𝑆 ⊆ ℂ)    &   (𝜑𝐹:𝐴⟶ℂ)    &   (𝜑𝐴𝑆)       ((𝜑𝐵(𝑆 D 𝐹)𝐶) → 𝐶 ∈ ℂ)

Theoremdvbssntrcntop 12862 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‘𝐽)‘𝐴))

Theoremdvbss 12863 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 𝐹) ⊆ 𝐴)

Theoremdvbsssg 12864 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 𝐹) ⊆ 𝑆)

Theoremrecnprss 12865 Both and are subsets of . (Contributed by Mario Carneiro, 10-Feb-2015.)
(𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Theoremdvfgg 12866 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 𝐹)⟶ℂ)

Theoremdvfpm 12867 The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.)
(𝐹 ∈ (ℂ ↑pm ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ)

Theoremdvfcnpm 12868 The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.)
(𝐹 ∈ (ℂ ↑pm ℂ) → (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ)

Theoremdvidlemap 12869* Lemma for dvid 12871 and dvconst 12870. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
(𝜑𝐹:ℂ⟶ℂ)    &   ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 # 𝑥)) → (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥)) = 𝐵)    &   𝐵 ∈ ℂ       (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵}))

Theoremdvconst 12870 Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
(𝐴 ∈ ℂ → (ℂ D (ℂ × {𝐴})) = (ℂ × {0}))

Theoremdvid 12871 Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
(ℂ D ( I ↾ ℂ)) = (ℂ × {1})

Theoremdvcnp2cntop 12872 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 𝐾)‘𝐵))

Theoremdvcn 12873 A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
(((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ dom (𝑆 D 𝐹) = 𝐴) → 𝐹 ∈ (𝐴cn→ℂ))

Theoremdvaddxxbr 12874 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 (𝐹𝑓 + 𝐺))(𝐾 + 𝐿))

Theoremdvmulxxbr 12875 The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 12877. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
(𝜑𝐹:𝑋⟶ℂ)    &   (𝜑𝑋𝑆)    &   (𝜑𝐺:𝑋⟶ℂ)    &   (𝜑𝑆 ⊆ ℂ)    &   (𝜑𝐶(𝑆 D 𝐹)𝐾)    &   (𝜑𝐶(𝑆 D 𝐺)𝐿)    &   𝐽 = (MetOpen‘(abs ∘ − ))       (𝜑𝐶(𝑆 D (𝐹𝑓 · 𝐺))((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))))

Theoremdvaddxx 12876 The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 12874. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
(𝜑𝐹:𝑋⟶ℂ)    &   (𝜑𝑋𝑆)    &   (𝜑𝐺:𝑋⟶ℂ)    &   (𝜑𝑆 ∈ {ℝ, ℂ})    &   (𝜑𝐶 ∈ dom (𝑆 D 𝐹))    &   (𝜑𝐶 ∈ dom (𝑆 D 𝐺))       (𝜑 → ((𝑆 D (𝐹𝑓 + 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘𝐶) + ((𝑆 D 𝐺)‘𝐶)))

Theoremdvmulxx 12877 The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 12875. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
(𝜑𝐹:𝑋⟶ℂ)    &   (𝜑𝑋𝑆)    &   (𝜑𝐺:𝑋⟶ℂ)    &   (𝜑𝑆 ∈ {ℝ, ℂ})    &   (𝜑𝐶 ∈ dom (𝑆 D 𝐹))    &   (𝜑𝐶 ∈ dom (𝑆 D 𝐺))       (𝜑 → ((𝑆 D (𝐹𝑓 · 𝐺))‘𝐶) = ((((𝑆 D 𝐹)‘𝐶) · (𝐺𝐶)) + (((𝑆 D 𝐺)‘𝐶) · (𝐹𝐶))))

Theoremdviaddf 12878 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 𝐺)))

Theoremdvimulf 12879 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 𝐺) ∘𝑓 · 𝐹)))

Theoremdvcoapbr 12880* 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 (𝐹𝐺))(𝐾 · 𝐿))

Theoremdvcjbr 12881 The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 12882. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
(𝜑𝐹:𝑋⟶ℂ)    &   (𝜑𝑋 ⊆ ℝ)    &   (𝜑𝐶 ∈ dom (ℝ D 𝐹))       (𝜑𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶)))

Theoremdvcj 12882 The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 12881. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → (ℝ D (∗ ∘ 𝐹)) = (∗ ∘ (ℝ D 𝐹)))

Theoremdvfre 12883 The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014.)
((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)

Theoremdvexp 12884* Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
(𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))

Theoremdvexp2 12885* 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))))))

Theoremdvrecap 12886* Derivative of the reciprocal function. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
(𝐴 ∈ ℂ → (ℂ D (𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 0} ↦ (𝐴 / 𝑥))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 0} ↦ -(𝐴 / (𝑥↑2))))

Theoremdvmptidcn 12887 Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.)
(ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1)

Theoremdvmptccn 12888* Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 0))

Theoremdvmptclx 12889* Closure lemma for dvmptmulx 12891 and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
(𝜑𝑆 ∈ {ℝ, ℂ})    &   ((𝜑𝑥𝑋) → 𝐴 ∈ ℂ)    &   ((𝜑𝑥𝑋) → 𝐵𝑉)    &   (𝜑 → (𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵))    &   (𝜑𝑋𝑆)       ((𝜑𝑥𝑋) → 𝐵 ∈ ℂ)

Theoremdvmptaddx 12890* Function-builder for derivative, addition rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
(𝜑𝑆 ∈ {ℝ, ℂ})    &   ((𝜑𝑥𝑋) → 𝐴 ∈ ℂ)    &   ((𝜑𝑥𝑋) → 𝐵𝑉)    &   (𝜑 → (𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵))    &   (𝜑𝑋𝑆)    &   ((𝜑𝑥𝑋) → 𝐶 ∈ ℂ)    &   ((𝜑𝑥𝑋) → 𝐷𝑊)    &   (𝜑 → (𝑆 D (𝑥𝑋𝐶)) = (𝑥𝑋𝐷))       (𝜑 → (𝑆 D (𝑥𝑋 ↦ (𝐴 + 𝐶))) = (𝑥𝑋 ↦ (𝐵 + 𝐷)))

Theoremdvmptmulx 12891* Function-builder for derivative, product rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
(𝜑𝑆 ∈ {ℝ, ℂ})    &   ((𝜑𝑥𝑋) → 𝐴 ∈ ℂ)    &   ((𝜑𝑥𝑋) → 𝐵𝑉)    &   (𝜑 → (𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵))    &   (𝜑𝑋𝑆)    &   ((𝜑𝑥𝑋) → 𝐶 ∈ ℂ)    &   ((𝜑𝑥𝑋) → 𝐷𝑊)    &   (𝜑 → (𝑆 D (𝑥𝑋𝐶)) = (𝑥𝑋𝐷))       (𝜑 → (𝑆 D (𝑥𝑋 ↦ (𝐴 · 𝐶))) = (𝑥𝑋 ↦ ((𝐵 · 𝐶) + (𝐷 · 𝐴))))

Theoremdvmptcmulcn 12892* 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 (𝑥 ∈ ℂ ↦ (𝐶 · 𝐴))) = (𝑥 ∈ ℂ ↦ (𝐶 · 𝐵)))

Theoremdvmptnegcn 12893* Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
((𝜑𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ((𝜑𝑥 ∈ ℂ) → 𝐵𝑉)    &   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))       (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ -𝐴)) = (𝑥 ∈ ℂ ↦ -𝐵))

Theoremdvmptsubcn 12894* Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
((𝜑𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ((𝜑𝑥 ∈ ℂ) → 𝐵𝑉)    &   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))    &   ((𝜑𝑥 ∈ ℂ) → 𝐶 ∈ ℂ)    &   ((𝜑𝑥 ∈ ℂ) → 𝐷𝑊)    &   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐶)) = (𝑥 ∈ ℂ ↦ 𝐷))       (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴𝐶))) = (𝑥 ∈ ℂ ↦ (𝐵𝐷)))

Theoremdvmptcjx 12895* Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.)
((𝜑𝑥𝑋) → 𝐴 ∈ ℂ)    &   ((𝜑𝑥𝑋) → 𝐵𝑉)    &   (𝜑 → (ℝ D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵))    &   (𝜑𝑋 ⊆ ℝ)       (𝜑 → (ℝ D (𝑥𝑋 ↦ (∗‘𝐴))) = (𝑥𝑋 ↦ (∗‘𝐵)))

Theoremdveflem 12896 Derivative of the exponential function at 0. The key step in the proof is eftlub 11434, 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

Theoremdvef 12897 Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
(ℂ D exp) = exp

PART 9  BASIC REAL AND COMPLEX FUNCTIONS

9.1  Basic trigonometry

9.1.1  The exponential, sine, and cosine functions (cont.)

Theoremefcn 12898 The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
exp ∈ (ℂ–cn→ℂ)

Theoremsincn 12899 Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
sin ∈ (ℂ–cn→ℂ)

Theoremcoscn 12900 Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
cos ∈ (ℂ–cn→ℂ)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13452
 Copyright terms: Public domain < Previous  Next >