P. 263 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26201-26300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvmptsub 26201*	Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 − 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 − 𝐷)))
Theorem	dvmptcj 26202*	Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (∗‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (∗‘𝐵)))
Theorem	dvmptre 26203*	Function-builder for derivative, real part. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐵)))
Theorem	dvmptim 26204*	Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐵)))
Theorem	dvmptntr 26205*	Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → ((int‘𝐽)‘𝑋) = 𝑌)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)))
Theorem	dvmptco 26206*	Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷))    &   ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸)    &   ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))
Theorem	dvrecg 26207*	Derivative of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐵)) = (𝑥 ∈ 𝑋 ↦ 𝐶))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵))) = (𝑥 ∈ 𝑋 ↦ -((𝐴 · 𝐶) / (𝐵↑2))))
Theorem	dvmptdiv 26208*	Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (((𝐵 · 𝐶) − (𝐷 · 𝐴)) / (𝐶↑2))))
Theorem	dvmptfsum 26209*	Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵))
Theorem	dvcnvlem 26210	Lemma for dvcnvre 26253. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)    &   ⊢ (𝜑 → ◡𝐹 ∈ (𝑌–cn→𝑋))    &   ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶)(𝑆 D ◡𝐹)(1 / ((𝑆 D 𝐹)‘𝐶)))
Theorem	dvcnv 26211*	A weak version of dvcnvre 26253, valid for both real and complex domains but under the hypothesis that the inverse function is already known to be continuous, and the image set is known to be open. A more advanced proof can show that these conditions are unnecessary. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)    &   ⊢ (𝜑 → ◡𝐹 ∈ (𝑌–cn→𝑋))    &   ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (𝑆 D 𝐹))    ⇒   ⊢ (𝜑 → (𝑆 D ◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((𝑆 D 𝐹)‘(◡𝐹‘𝑥)))))
Theorem	dvexp3 26212*	Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝑁 ∈ ℤ → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥↑𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
Theorem	dveflem 26213	Derivative of the exponential function at 0. The key step in the proof is eftlub 16203, 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 26214	Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
⊢ (ℂ D exp) = exp
Theorem	dvsincos 26215	Derivative of the sine and cosine functions. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ ((ℂ D sin) = cos ∧ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥)))
Theorem	dvsin 26216	Derivative of the sine function. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ (ℂ D sin) = cos
Theorem	dvcos 26217	Derivative of the cosine function. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥))
13.3.1.2  Results on real differentiation
Theorem	dvferm1lem 26218*	Lemma for dvferm 26222. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹))    &   ⊢ (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈))    &   ⊢ (𝜑 → 0 < ((ℝ D 𝐹)‘𝑈))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))    &   ⊢ 𝑆 = ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2)    ⇒   ⊢ ¬ 𝜑
Theorem	dvferm1 26219*	One-sided version of dvferm 26222. A point 𝑈 which is the local maximum of its right neighborhood has derivative at most zero. (Contributed by Mario Carneiro, 24-Feb-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹))    &   ⊢ (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈))    ⇒   ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ≤ 0)
Theorem	dvferm2lem 26220*	Lemma for dvferm 26222. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹))    &   ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈))    &   ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) < 0)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))    &   ⊢ 𝑆 = ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2)    ⇒   ⊢ ¬ 𝜑
Theorem	dvferm2 26221*	One-sided version of dvferm 26222. A point 𝑈 which is the local maximum of its left neighborhood has derivative at least zero. (Contributed by Mario Carneiro, 24-Feb-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹))    &   ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈))    ⇒   ⊢ (𝜑 → 0 ≤ ((ℝ D 𝐹)‘𝑈))
Theorem	dvferm 26222*	Fermat's theorem on stationary points. A point 𝑈 which is a local maximum has derivative equal to zero. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ (𝜑 → 𝐹:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹))    &   ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈))    ⇒   ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) = 0)
Theorem	rollelem 26223*	Lemma for rolle 26224. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ¬ 𝑈 ∈ {𝐴, 𝐵})    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
Theorem	rolle 26224*	Rolle's theorem. If 𝐹 is a real continuous function on [𝐴, 𝐵] which is differentiable on (𝐴, 𝐵), and 𝐹(𝐴) = 𝐹(𝐵), then there is some 𝑥 ∈ (𝐴, 𝐵) such that (ℝ D 𝐹)‘𝑥 = 0. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
Theorem	cmvth 26225*	Cauchy's Mean Value Theorem. If 𝐹, 𝐺 are real continuous functions on [𝐴, 𝐵] differentiable on (𝐴, 𝐵), then there is some 𝑥 ∈ (𝐴, 𝐵) such that 𝐹' (𝑥) / 𝐺' (𝑥) = (𝐹(𝐴) − 𝐹(𝐵)) / (𝐺(𝐴) − 𝐺(𝐵)). (We express the condition without division, so that we need no nonzero constraints.) (Contributed by Mario Carneiro, 29-Dec-2016.) Avoid ax-mulf 11208. (Revised by GG, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)))
Theorem	mvth 26226*	The Mean Value Theorem. If 𝐹 is a real continuous function on [𝐴, 𝐵] which is differentiable on (𝐴, 𝐵), then there is some 𝑥 ∈ (𝐴, 𝐵) such that (ℝ D 𝐹)‘𝑥 is equal to the average slope over [𝐴, 𝐵]. This is Metamath 100 proof #75. (Contributed by Mario Carneiro, 1-Sep-2014.) (Proof shortened by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)))
Theorem	dvlip 26227*	A function with derivative bounded by 𝑀 is 𝑀-Lipschitz continuous. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹‘𝑋) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑋 − 𝑌))))
Theorem	dvlipcn 26228*	A complex function with derivative bounded by 𝑀 on an open ball is 𝑀-Lipschitz continuous. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ (𝜑 → 𝑋 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)    &   ⊢ (𝜑 → 𝐵 ⊆ dom (ℂ D 𝐹))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)    ⇒   ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
Theorem	dvlip2 26229*	Combine the results of dvlip 26227 and dvlipcn 26228 into one. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ 𝐽 = ((abs ∘ − ) ↾ (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ 𝐵 = (𝐴(ball‘𝐽)𝑅)    &   ⊢ (𝜑 → 𝐵 ⊆ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀)    ⇒   ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
Theorem	c1liplem1 26230*	Lemma for c1lip1 26231. (Contributed by Stefan O'Rear, 15-Nov-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm ℝ))    &   ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ 𝐾 = sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < )    ⇒   ⊢ (𝜑 → (𝐾 ∈ ℝ ∧ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥))))))
Theorem	c1lip1 26231*	C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm ℝ))    &   ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑘 · (abs‘(𝑦 − 𝑥))))
Theorem	c1lip2 26232*	C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝓑C𝑛‘ℝ)‘1))    &   ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑘 · (abs‘(𝑦 − 𝑥))))
Theorem	c1lip3 26233*	C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹 ↾ ℝ) ∈ ((𝓑C𝑛‘ℝ)‘1))    &   ⊢ (𝜑 → (𝐹 “ ℝ) ⊆ ℝ)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑘 · (abs‘(𝑦 − 𝑥))))
Theorem	dveq0 26234	If a continuous function has zero derivative at all points on the interior of a closed interval, then it must be a constant function. (Contributed by Mario Carneiro, 2-Sep-2014.) (Proof shortened by Mario Carneiro, 3-Mar-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D 𝐹) = ((𝐴(,)𝐵) × {0}))    ⇒   ⊢ (𝜑 → 𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)}))
Theorem	dv11cn 26235	Two functions defined on a ball whose derivatives are the same and which are equal at any given point 𝐶 in the ball must be equal everywhere. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ 𝑋 = (𝐴(ball‘(abs ∘ − ))𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → dom (ℂ D 𝐹) = 𝑋)    &   ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ D 𝐺))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → (𝐹‘𝐶) = (𝐺‘𝐶))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	dvgt0lem1 26236	Lemma for dvgt0 26238 and dvlt0 26239. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶𝑆)    ⇒   ⊢ (((𝜑 ∧ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵))) ∧ 𝑋 < 𝑌) → (((𝐹‘𝑌) − (𝐹‘𝑋)) / (𝑌 − 𝑋)) ∈ 𝑆)
Theorem	dvgt0lem2 26237*	Lemma for dvgt0 26238 and dvlt0 26239. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶𝑆)    &   ⊢ 𝑂 Or ℝ    &   ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹‘𝑥)𝑂(𝐹‘𝑦))    ⇒   ⊢ (𝜑 → 𝐹 Isom < , 𝑂 ((𝐴[,]𝐵), ran 𝐹))
Theorem	dvgt0 26238	A function on a closed interval with positive derivative is increasing. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ+)    ⇒   ⊢ (𝜑 → 𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹))
Theorem	dvlt0 26239	A function on a closed interval with negative derivative is decreasing. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶(-∞(,)0))    ⇒   ⊢ (𝜑 → 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))
Theorem	dvge0 26240	A function on a closed interval with nonnegative derivative is weakly increasing. (Contributed by Mario Carneiro, 30-Apr-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ≤ (𝐹‘𝑌))
Theorem	dvle 26241*	If 𝐴(𝑥), 𝐶(𝑥) are differentiable functions and 𝐴‘ ≤ 𝐶‘, then for 𝑥 ≤ 𝑦, 𝐴(𝑦) − 𝐴(𝑥) ≤ 𝐶(𝑦) − 𝐶(𝑥). (Contributed by Mario Carneiro, 16-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ≤ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑀[,]𝑁))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑀[,]𝑁))    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝑥 = 𝑋 → 𝐴 = 𝑃)    &   ⊢ (𝑥 = 𝑋 → 𝐶 = 𝑄)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝑅)    &   ⊢ (𝑥 = 𝑌 → 𝐶 = 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 − 𝑃) ≤ (𝑆 − 𝑄))
Theorem	dvivthlem1 26242*	Lemma for dvivth 26244. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑀 < 𝑁)    &   ⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)))    &   ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶)
Theorem	dvivthlem2 26243*	Lemma for dvivth 26244. (Contributed by Mario Carneiro, 20-Feb-2015.)
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑀 < 𝑁)    &   ⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)))    &   ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦)))    ⇒   ⊢ (𝜑 → 𝐶 ∈ ran (ℝ D 𝐹))
Theorem	dvivth 26244	Darboux' theorem, or the intermediate value theorem for derivatives. A differentiable function's derivative satisfies the intermediate value property, even though it may not be continuous (so that ivthicc 25692 does not directly apply). (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹))
Theorem	dvne0 26245	A function on a closed interval with nonzero derivative is either monotone increasing or monotone decreasing. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))    ⇒   ⊢ (𝜑 → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹)))
Theorem	dvne0f1 26246	A function on a closed interval with nonzero derivative is one-to-one. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))    ⇒   ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)–1-1→ℝ)
Theorem	lhop1lem 26247*	Lemma for lhop1 26248. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)    &   ⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ)    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐴))    &   ⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝐴))    &   ⊢ (𝜑 → ¬ 0 ∈ ran 𝐺)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))    &   ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐴))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴(,)𝐷))    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)    &   ⊢ 𝑅 = (𝐴 + (𝑟 / 2))    ⇒   ⊢ (𝜑 → (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) < (2 · 𝐸))
Theorem	lhop1 26248*	L'Hôpital's Rule for limits from the right. If 𝐹 and 𝐺 are differentiable real functions on (𝐴, 𝐵), and 𝐹 and 𝐺 both approach 0 at 𝐴, and 𝐺(𝑥) and 𝐺' (𝑥) are not zero on (𝐴, 𝐵), and the limit of 𝐹' (𝑥) / 𝐺' (𝑥) at 𝐴 is 𝐶, then the limit 𝐹(𝑥) / 𝐺(𝑥) at 𝐴 also exists and equals 𝐶. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)    &   ⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ)    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐴))    &   ⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝐴))    &   ⊢ (𝜑 → ¬ 0 ∈ ran 𝐺)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))    &   ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐴))    ⇒   ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐴))
Theorem	lhop2 26249*	L'Hôpital's Rule for limits from the left. If 𝐹 and 𝐺 are differentiable real functions on (𝐴, 𝐵), and 𝐹 and 𝐺 both approach 0 at 𝐵, and 𝐺(𝑥) and 𝐺' (𝑥) are not zero on (𝐴, 𝐵), and the limit of 𝐹' (𝑥) / 𝐺' (𝑥) at 𝐵 is 𝐶, then the limit 𝐹(𝑥) / 𝐺(𝑥) at 𝐵 also exists and equals 𝐶. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)    &   ⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ)    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝐵))    &   ⊢ (𝜑 → ¬ 0 ∈ ran 𝐺)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))    &   ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵))    ⇒   ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵))
Theorem	lhop 26250*	L'Hôpital's Rule. If 𝐼 is an open set of the reals, 𝐹 and 𝐺 are real functions on 𝐴 containing all of 𝐼 except possibly 𝐵, which are differentiable everywhere on 𝐼 ∖ {𝐵}, 𝐹 and 𝐺 both approach 0, and the limit of 𝐹' (𝑥) / 𝐺' (𝑥) at 𝐵 is 𝐶, then the limit 𝐹(𝑥) / 𝐺(𝑥) at 𝐵 also exists and equals 𝐶. This is Metamath 100 proof #64. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐼 ∈ (topGen‘ran (,)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐼)    &   ⊢ 𝐷 = (𝐼 ∖ {𝐵})    &   ⊢ (𝜑 → 𝐷 ⊆ dom (ℝ D 𝐹))    &   ⊢ (𝜑 → 𝐷 ⊆ dom (ℝ D 𝐺))    &   ⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝐵))    &   ⊢ (𝜑 → ¬ 0 ∈ (𝐺 “ 𝐷))    &   ⊢ (𝜑 → ¬ 0 ∈ ((ℝ D 𝐺) “ 𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵))    ⇒   ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵))
Theorem	dvcnvrelem1 26251	Lemma for dvcnvre 26253. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))    &   ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))))
Theorem	dvcnvrelem2 26252	Lemma for dvcnvre 26253. (Contributed by Mario Carneiro, 19-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))    &   ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋)    &   ⊢ 𝑇 = (topGen‘ran (,))    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑀 = (𝐽 ↾t 𝑋)    &   ⊢ 𝑁 = (𝐽 ↾t 𝑌)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐶) ∈ ((int‘𝑇)‘𝑌) ∧ ◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶))))
Theorem	dvcnvre 26253*	The derivative rule for inverse functions. If 𝐹 is a continuous and differentiable bijective function from 𝑋 to 𝑌 which never has derivative 0, then ◡𝐹 is also differentiable, and its derivative is the reciprocal of the derivative of 𝐹. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))    &   ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)    ⇒   ⊢ (𝜑 → (ℝ D ◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((ℝ D 𝐹)‘(◡𝐹‘𝑥)))))
Theorem	dvcvx 26254	A real function with strictly increasing derivative is strictly convex. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D 𝐹) Isom < , < ((𝐴(,)𝐵), 𝑊))    &   ⊢ (𝜑 → 𝑇 ∈ (0(,)1))    &   ⊢ 𝐶 = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) < ((𝑇 · (𝐹‘𝐴)) + ((1 − 𝑇) · (𝐹‘𝐵))))
Theorem	dvfsumle 26255*	Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016.) Avoid ax-mulf 11208. (Revised by GG, 16-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))    &   ⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝑋 ≤ 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ (𝐷 − 𝐶))
Theorem	dvfsumge 26256*	Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))    &   ⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝐵 ≤ 𝑋)    ⇒   ⊢ (𝜑 → (𝐷 − 𝐶) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑋)
Theorem	dvfsumabs 26257*	Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))    &   ⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → (abs‘(𝑋 − 𝐵)) ≤ 𝑌)    ⇒   ⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑌)
Theorem	dvmptrecl 26258*	Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ (𝜑 → 𝑆 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ)
Theorem	dvfsumrlimf 26259*	Lemma for dvfsumrlim 26265. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    ⇒   ⊢ (𝜑 → 𝐺:𝑆⟶ℝ)
Theorem	dvfsumlem1 26260*	Lemma for dvfsumrlim 26265. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑈)    &   ⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1))    ⇒   ⊢ (𝜑 → (𝐻‘𝑌) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
Theorem	dvfsumlem2 26261*	Lemma for dvfsumrlim 26265. (Contributed by Mario Carneiro, 17-May-2016.) Avoid ax-mulf 11208. (Revised by GG, 16-Mar-2025.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑈)    &   ⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1))    ⇒   ⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵)))
Theorem	dvfsumlem3 26262*	Lemma for dvfsumrlim 26265. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵)))
Theorem	dvfsumlem4 26263*	Lemma for dvfsumrlim 26265. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈)) → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑈)    ⇒   ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐵)
Theorem	dvfsumrlimge0 26264*	Lemma for dvfsumrlim 26265. Satisfy the assumption of dvfsumlem4 26263. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵)
Theorem	dvfsumrlim 26265*	Compare a finite sum to an integral (the integral here is given as a function with a known derivative). The statement here says that if 𝑥 ∈ 𝑆 ↦ 𝐵 is a decreasing function with antiderivative 𝐴 converging to zero, then the difference between Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐵(𝑘) and 𝐴(𝑥) = ∫𝑢 ∈ (𝑀[,]𝑥)𝐵(𝑢) d𝑢 converges to a constant limit value, with the remainder term bounded by 𝐵(𝑥). (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0)    ⇒   ⊢ (𝜑 → 𝐺 ∈ dom ⇝𝑟 )
Theorem	dvfsumrlim2 26266*	Compare a finite sum to an integral (the integral here is given as a function with a known derivative). The statement here says that if 𝑥 ∈ 𝑆 ↦ 𝐵 is a decreasing function with antiderivative 𝐴 converging to zero, then the difference between Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐵(𝑘) and ∫𝑢 ∈ (𝑀[,]𝑥)𝐵(𝑢) d𝑢 = 𝐴(𝑥) converges to a constant limit value, with the remainder term bounded by 𝐵(𝑥). (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    ⇒   ⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (abs‘((𝐺‘𝑋) − 𝐿)) ≤ ⦋𝑋 / 𝑥⦌𝐵)
Theorem	dvfsumrlim3 26267*	Conjoin the statements of dvfsumrlim 26265 and dvfsumrlim2 26266. (This is useful as a target for lemmas, because the hypotheses to this theorem are complex, and we don't want to repeat ourselves.) (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0)    &   ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐸)    ⇒   ⊢ (𝜑 → (𝐺:𝑆⟶ℝ ∧ 𝐺 ∈ dom ⇝𝑟 ∧ ((𝐺 ⇝𝑟 𝐿 ∧ 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋) → (abs‘((𝐺‘𝑋) − 𝐿)) ≤ 𝐸)))
Theorem	dvfsum2 26268*	The reverse of dvfsumrlim 26265, when comparing a finite sum of increasing terms to an integral. In this case there is no point in stating the limit properties, because the terms of the sum aren't approaching zero, but there is nevertheless still a natural asymptotic statement that can be made. (Contributed by Mario Carneiro, 20-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ≤ 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑈)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐸)    ⇒   ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ 𝐸)
Theorem	ftc1lem1 26269*	Lemma for ftc1a 26271 and ftc1 26276. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡)
Theorem	ftc1lem2 26270*	Lemma for ftc1 26276. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    ⇒   ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ)
Theorem	ftc1a 26271*	The Fundamental Theorem of Calculus, part one. The function 𝐺 formed by varying the right endpoint of an integral of 𝐹 is continuous if 𝐹 is integrable. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Theorem	ftc1lem3 26272*	Lemma for ftc1 26276. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶))    &   ⊢ 𝐽 = (𝐿 ↾t ℝ)    &   ⊢ 𝐾 = (𝐿 ↾t 𝐷)    &   ⊢ 𝐿 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
Theorem	ftc1lem4 26273*	Lemma for ftc1 26276. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶))    &   ⊢ 𝐽 = (𝐿 ↾t ℝ)    &   ⊢ 𝐾 = (𝐿 ↾t 𝐷)    &   ⊢ 𝐿 = (TopOpen‘ℂfld)    &   ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((abs‘(𝑦 − 𝐶)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) < 𝑅)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (abs‘(𝑌 − 𝐶)) < 𝑅)    ⇒   ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝐶))) < 𝐸)
Theorem	ftc1lem5 26274*	Lemma for ftc1 26276. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶))    &   ⊢ 𝐽 = (𝐿 ↾t ℝ)    &   ⊢ 𝐾 = (𝐿 ↾t 𝐷)    &   ⊢ 𝐿 = (TopOpen‘ℂfld)    &   ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((abs‘(𝑦 − 𝐶)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) < 𝑅)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐶) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) < 𝐸)
Theorem	ftc1lem6 26275*	Lemma for ftc1 26276. (Contributed by Mario Carneiro, 14-Aug-2014.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶))    &   ⊢ 𝐽 = (𝐿 ↾t ℝ)    &   ⊢ 𝐾 = (𝐿 ↾t 𝐷)    &   ⊢ 𝐿 = (TopOpen‘ℂfld)    &   ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐻 limℂ 𝐶))
Theorem	ftc1 26276*	The Fundamental Theorem of Calculus, part one. The function formed by varying the right endpoint of an integral is differentiable at 𝐶 with derivative 𝐹(𝐶) if the original function is continuous at 𝐶. This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶))    &   ⊢ 𝐽 = (𝐿 ↾t ℝ)    &   ⊢ 𝐾 = (𝐿 ↾t 𝐷)    &   ⊢ 𝐿 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → 𝐶(ℝ D 𝐺)(𝐹‘𝐶))
Theorem	ftc1cn 26277*	Strengthen the assumptions of ftc1 26276 to when the function 𝐹 is continuous on the entire interval (𝐴, 𝐵); in this case we can calculate D 𝐺 exactly. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (ℝ D 𝐺) = 𝐹)
Theorem	ftc2 26278*	The Fundamental Theorem of Calculus, part two. If 𝐹 is a function continuous on [𝐴, 𝐵] and continuously differentiable on (𝐴, 𝐵), then the integral of the derivative of 𝐹 is equal to 𝐹(𝐵) − 𝐹(𝐴). This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 2-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	ftc2ditglem 26279*	Lemma for ftc2ditg 26280. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	ftc2ditg 26280*	Directed integral analogue of ftc2 26278. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ))    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	itgparts 26281*	Integration by parts. If 𝐵(𝑥) is the derivative of 𝐴(𝑥) and 𝐷(𝑥) is the derivative of 𝐶(𝑥), and 𝐸 = (𝐴 · 𝐵)(𝑋) and 𝐹 = (𝐴 · 𝐵)(𝑌), then under suitable integrability and differentiability assumptions, the integral of 𝐴 · 𝐷 from 𝑋 to 𝑌 is equal to 𝐹 − 𝐸 minus the integral of 𝐵 · 𝐶. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) ∈ ((𝑋[,]𝑌)–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ ((𝑋(,)𝑌)–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐴 · 𝐷)) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐵 · 𝐶)) ∈ 𝐿1)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝐴 · 𝐶) = 𝐸)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝐴 · 𝐶) = 𝐹)    ⇒   ⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐴 · 𝐷) d𝑥 = ((𝐹 − 𝐸) − ∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥))
Theorem	itgsubstlem 26282*	Lemma for itgsubst 26283. (Contributed by Mario Carneiro, 12-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ*)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1))    &   ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))    &   ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)    &   ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))    ⇒   ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)
Theorem	itgsubst 26283*	Integration by 𝑢-substitution. If 𝐴(𝑥) is a continuous, differentiable function from [𝑋, 𝑌] to (𝑍, 𝑊), whose derivative is continuous and integrable, and 𝐶(𝑢) is a continuous function on (𝑍, 𝑊), then the integral of 𝐶(𝑢) from 𝐾 = 𝐴(𝑋) to 𝐿 = 𝐴(𝑌) is equal to the integral of 𝐶(𝐴(𝑥)) D 𝐴(𝑥) from 𝑋 to 𝑌. In this part of the proof we discharge the assumptions in itgsubstlem 26282, which use the fact that (𝑍, 𝑊) is open to shrink the interval a little to (𝑀, 𝑁) where 𝑍 < 𝑀 < 𝑁 < 𝑊- this is possible because 𝐴(𝑥) is a continuous function on a closed interval, so its range is in fact a closed interval, and we have some wiggle room on the edges. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ*)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1))    &   ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))    &   ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)    &   ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)    ⇒   ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)
Theorem	itgpowd 26284*	The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019.) (Revised by Thierry Arnoux, 14-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥 = (((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1))) / (𝑁 + 1)))
PART 14  BASIC REAL AND COMPLEX FUNCTIONS
14.1  Polynomials
14.1.1  Polynomial degrees
Syntax	cmdg 26285	Multivariate polynomial degree.
class mDeg
Syntax	cdg1 26286	Univariate polynomial degree.
class deg1
Definition	df-mdeg 26287*	Define the degree of a polynomial. Note (SO): as an experiment I am using a definition which makes the degree of the zero polynomial -∞, contrary to the convention used in df-dgr 26423. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.)
⊢ mDeg = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld Σg ℎ)), ℝ*, < )))
Definition	df-deg1 26288	Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ deg1 = (𝑟 ∈ V ↦ (1o mDeg 𝑟))
Theorem	reldmmdeg 26289	Multivariate degree is a binary operation. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ Rel dom mDeg
Theorem	tdeglem1 26290*	Functionality of the total degree helper function. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) Remove sethood antecedent. (Revised by SN, 7-Aug-2024.)
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ 𝐻:𝐴⟶ℕ0
Theorem	tdeglem3 26291*	Additivity of the total degree helper function. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.)
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐻‘(𝑋 ∘f + 𝑌)) = ((𝐻‘𝑋) + (𝐻‘𝑌)))
Theorem	tdeglem4 26292*	There is only one multi-index with total degree 0. (Contributed by Stefan O'Rear, 29-Mar-2015.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.)
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ (𝑋 ∈ 𝐴 → ((𝐻‘𝑋) = 0 ↔ 𝑋 = (𝐼 × {0})))
Theorem	tdeglem2 26293	Simplification of total degree for the univariate case. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ (ℎ ∈ (ℕ0 ↑m 1o) ↦ (ℎ‘∅)) = (ℎ ∈ (ℕ0 ↑m 1o) ↦ (ℂfld Σg ℎ))
Theorem	mdegfval 26294*	Value of the multivariate degree function. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ 𝐷 = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*, < ))
Theorem	mdegval 26295*	Value of the multivariate degree function at some particular polynomial. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*, < ))
Theorem	mdegleb 26296*	Property of being of limited degree. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))
Theorem	mdeglt 26297*	If there is an upper limit on the degree of a polynomial that is lower than the degree of some exponent bag, then that exponent bag is unrepresented in the polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐷‘𝐹) < (𝐻‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) = 0 )
Theorem	mdegldg 26298*	A nonzero polynomial has some coefficient which witnesses its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    &   ⊢ 𝑌 = (0g‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹)))
Theorem	mdegxrcl 26299	Closure of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ ℝ*)
Theorem	mdegxrf 26300	Functionality of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ 𝐷:𝐵⟶ℝ*