P. 238 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23701-23800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvaddbr 23701	The sum rule for derivatives at a point. For the (simpler but more limited) function version, see dvadd 23703. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 + 𝐺))(𝐾 + 𝐿))
Theorem	dvmulbr 23702	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 23704. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)    &   ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))
Theorem	dvadd 23703	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddbr 23701. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 + 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘𝐶) + ((𝑆 D 𝐺)‘𝐶)))
Theorem	dvmul 23704	The product rule for derivatives at a point. For the (more general) relation version, see dvmulbr 23702. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 · 𝐺))‘𝐶) = ((((𝑆 D 𝐹)‘𝐶) · (𝐺‘𝐶)) + (((𝑆 D 𝐺)‘𝐶) · (𝐹‘𝐶))))
Theorem	dvaddf 23705	The sum rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)    &   ⊢ (𝜑 → dom (𝑆 D 𝐺) = 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 + 𝐺)) = ((𝑆 D 𝐹) ∘𝑓 + (𝑆 D 𝐺)))
Theorem	dvmulf 23706	The product rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)    &   ⊢ (𝜑 → dom (𝑆 D 𝐺) = 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 · 𝐺)) = (((𝑆 D 𝐹) ∘𝑓 · 𝐺) ∘𝑓 + ((𝑆 D 𝐺) ∘𝑓 · 𝐹)))
Theorem	dvcmul 23707	The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    ⇒   ⊢ (𝜑 → ((𝑆 D ((𝑆 × {𝐴}) ∘𝑓 · 𝐹))‘𝐶) = (𝐴 · ((𝑆 D 𝐹)‘𝐶)))
Theorem	dvcmulf 23708	The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ∘𝑓 · 𝐹)) = ((𝑆 × {𝐴}) ∘𝑓 · (𝑆 D 𝐹)))
Theorem	dvcobr 23709	The chain rule for derivatives at a point. For the (simpler but more limited) function version, see dvco 23710. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶𝑋)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑇 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐺‘𝐶)(𝑆 D 𝐹)𝐾)    &   ⊢ (𝜑 → 𝐶(𝑇 D 𝐺)𝐿)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → 𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿))
Theorem	dvco 23710	The chain rule for derivatives at a point. For the (more general) relation version, see dvcobr 23709. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝑌⟶𝑋)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → (𝐺‘𝐶) ∈ dom (𝑆 D 𝐹))    &   ⊢ (𝜑 → 𝐶 ∈ dom (𝑇 D 𝐺))    ⇒   ⊢ (𝜑 → ((𝑇 D (𝐹 ∘ 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘(𝐺‘𝐶)) · ((𝑇 D 𝐺)‘𝐶)))
Theorem	dvcof 23711	The chain rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 10-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐺:𝑌⟶𝑋)    &   ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)    &   ⊢ (𝜑 → dom (𝑇 D 𝐺) = 𝑌)    ⇒   ⊢ (𝜑 → (𝑇 D (𝐹 ∘ 𝐺)) = (((𝑆 D 𝐹) ∘ 𝐺) ∘𝑓 · (𝑇 D 𝐺)))
Theorem	dvcjbr 23712	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 23713. (This doesn't follow from dvcobr 23709 because ∗ is not a function on the reals, and even if we used complex derivatives, ∗ is not complex-differentiable.) (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ dom (ℝ D 𝐹))    ⇒   ⊢ (𝜑 → 𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶)))
Theorem	dvcj 23713	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 23712. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → (ℝ D (∗ ∘ 𝐹)) = (∗ ∘ (ℝ D 𝐹)))
Theorem	dvfre 23714	The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
Theorem	dvnfre 23715	The 𝑁-th derivative of a real function is real. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑁 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑁):dom ((ℝ D𝑛 𝐹)‘𝑁)⟶ℝ)
Theorem	dvexp 23716*	Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
Theorem	dvexp2 23717*	Derivative of an exponential, possibly zero power. (Contributed by Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
⊢ (𝑁 ∈ ℕ0 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1))))))
Theorem	dvrec 23718*	Derivative of the reciprocal function. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐴 ∈ ℂ → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2))))
Theorem	dvmptres3 23719*	Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑆 ∩ 𝑋) = 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵))
Theorem	dvmptid 23720*	Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑆 ↦ 𝑥)) = (𝑥 ∈ 𝑆 ↦ 1))
Theorem	dvmptc 23721*	Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 0))
Theorem	dvmptcl 23722*	Closure lemma for dvmptcmul 23727 and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ)
Theorem	dvmptadd 23723*	Function-builder for derivative, addition rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 + 𝐷)))
Theorem	dvmptmul 23724*	Function-builder for derivative, product rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐶))) = (𝑥 ∈ 𝑋 ↦ ((𝐵 · 𝐶) + (𝐷 · 𝐴))))
Theorem	dvmptres2 23725*	Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝑍 ⊆ 𝑋)    &   ⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → ((int‘𝐽)‘𝑍) = 𝑌)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑍 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵))
Theorem	dvmptres 23726*	Function-builder for derivative: restrict a derivative to an open subset. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐽)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵))
Theorem	dvmptcmul 23727*	Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐶 · 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝐶 · 𝐵)))
Theorem	dvmptdivc 23728*	Function-builder for derivative, division rule for constant divisor. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶)))
Theorem	dvmptneg 23729*	Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ -𝐴)) = (𝑥 ∈ 𝑋 ↦ -𝐵))
Theorem	dvmptsub 23730*	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 23731*	Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (∗‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (∗‘𝐵)))
Theorem	dvmptre 23732*	Function-builder for derivative, real part. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐵)))
Theorem	dvmptim 23733*	Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐵)))
Theorem	dvmptntr 23734*	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 23735*	Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷))    &   ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸)    &   ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵)))
Theorem	dvrecg 23736*	Derivative of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐵)) = (𝑥 ∈ 𝑋 ↦ 𝐶))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵))) = (𝑥 ∈ 𝑋 ↦ -((𝐴 · 𝐶) / (𝐵↑2))))
Theorem	dvmptdiv 23737*	Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (((𝐵 · 𝐶) − (𝐷 · 𝐴)) / (𝐶↑2))))
Theorem	dvmptfsum 23738*	Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵))
Theorem	dvcnvlem 23739	Lemma for dvcnvre 23782. (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 23740*	A weak version of dvcnvre 23782, 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 23741*	Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝑁 ∈ ℤ → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥↑𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
Theorem	dveflem 23742	Derivative of the exponential function at 0. The key step in the proof is eftlub 14839, 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 23743	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 23744	Derivative of the sine and cosine functions. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ ((ℂ D sin) = cos ∧ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥)))
Theorem	dvsin 23745	Derivative of the sine function. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ (ℂ D sin) = cos
Theorem	dvcos 23746	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 23747*	Lemma for dvferm 23751. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹))    &   ⊢ (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈))    &   ⊢ (𝜑 → 0 < ((ℝ D 𝐹)‘𝑈))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))    &   ⊢ 𝑆 = ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2)    ⇒   ⊢ ¬ 𝜑
Theorem	dvferm1 23748*	One-sided version of dvferm 23751. 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 23749*	Lemma for dvferm 23751. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹))    &   ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈))    &   ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) < 0)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))    &   ⊢ 𝑆 = ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2)    ⇒   ⊢ ¬ 𝜑
Theorem	dvferm2 23750*	One-sided version of dvferm 23751. 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 23751*	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 23752*	Lemma for rolle 23753. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ¬ 𝑈 ∈ {𝐴, 𝐵})    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
Theorem	rolle 23753*	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 23754*	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.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)))
Theorem	mvth 23755*	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 23756*	A function with derivative bounded by 𝑀 is Lipschitz continuous with Lipschitz constant equal to 𝑀. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹‘𝑋) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑋 − 𝑌))))
Theorem	dvlipcn 23757*	A complex function with derivative bounded by 𝑀 on an open ball is Lipschitz continuous with Lipschitz constant equal to 𝑀. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ (𝜑 → 𝑋 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)    &   ⊢ (𝜑 → 𝐵 ⊆ dom (ℂ D 𝐹))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)    ⇒   ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
Theorem	dvlip2 23758*	Combine the results of dvlip 23756 and dvlipcn 23757 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 23759*	Lemma for c1lip1 23760. (Contributed by Stefan O'Rear, 15-Nov-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm ℝ))    &   ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ 𝐾 = sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < )    ⇒   ⊢ (𝜑 → (𝐾 ∈ ℝ ∧ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥))))))
Theorem	c1lip1 23760*	C1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm ℝ))    &   ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑘 · (abs‘(𝑦 − 𝑥))))
Theorem	c1lip2 23761*	C1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((Cn‘ℝ)‘1))    &   ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑘 · (abs‘(𝑦 − 𝑥))))
Theorem	c1lip3 23762*	C1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹 ↾ ℝ) ∈ ((Cn‘ℝ)‘1))    &   ⊢ (𝜑 → (𝐹 “ ℝ) ⊆ ℝ)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑘 · (abs‘(𝑦 − 𝑥))))
Theorem	dveq0 23763	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 23764	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 23765	Lemma for dvgt0 23767 and dvlt0 23768. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶𝑆)    ⇒   ⊢ (((𝜑 ∧ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵))) ∧ 𝑋 < 𝑌) → (((𝐹‘𝑌) − (𝐹‘𝑋)) / (𝑌 − 𝑋)) ∈ 𝑆)
Theorem	dvgt0lem2 23766*	Lemma for dvgt0 23767 and dvlt0 23768. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶𝑆)    &   ⊢ 𝑂 Or ℝ    &   ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹‘𝑥)𝑂(𝐹‘𝑦))    ⇒   ⊢ (𝜑 → 𝐹 Isom < , 𝑂 ((𝐴[,]𝐵), ran 𝐹))
Theorem	dvgt0 23767	A function on a closed interval with positive derivative is increasing. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ+)    ⇒   ⊢ (𝜑 → 𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹))
Theorem	dvlt0 23768	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 23769	A function on a closed interval with nonnegative derivative is weakly increasing. (Contributed by Mario Carneiro, 30-Apr-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ≤ (𝐹‘𝑌))
Theorem	dvle 23770*	If 𝐴(𝑥), 𝐶(𝑥) are differentiable functions and 𝐴‘ ≤ 𝐶‘, then for 𝑥 ≤ 𝑦, 𝐴(𝑦) − 𝐴(𝑥) ≤ 𝐶(𝑦) − 𝐶(𝑥). (Contributed by Mario Carneiro, 16-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ≤ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑀[,]𝑁))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑀[,]𝑁))    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝑥 = 𝑋 → 𝐴 = 𝑃)    &   ⊢ (𝑥 = 𝑋 → 𝐶 = 𝑄)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝑅)    &   ⊢ (𝑥 = 𝑌 → 𝐶 = 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 − 𝑃) ≤ (𝑆 − 𝑄))
Theorem	dvivthlem1 23771*	Lemma for dvivth 23773. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑀 < 𝑁)    &   ⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)))    &   ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶)
Theorem	dvivthlem2 23772*	Lemma for dvivth 23773. (Contributed by Mario Carneiro, 20-Feb-2015.)
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑀 < 𝑁)    &   ⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)))    &   ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦)))    ⇒   ⊢ (𝜑 → 𝐶 ∈ ran (ℝ D 𝐹))
Theorem	dvivth 23773	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 23227 does not directly apply). (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹))
Theorem	dvne0 23774	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 23775	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 23776*	Lemma for lhop1 23777. (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 23777*	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 23778*	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 23779*	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 23780	Lemma for dvcnvre 23782. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ))    &   ⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋)    &   ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))    &   ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))))
Theorem	dvcnvrelem2 23781	Lemma for dvcnvre 23782. (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 23782*	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 23783	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 23784*	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	dvfsumge 23785*	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 23786*	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 23787*	Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ (𝜑 → 𝑆 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ)
Theorem	dvfsumrlimf 23788*	Lemma for dvfsumrlim 23794. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    ⇒   ⊢ (𝜑 → 𝐺:𝑆⟶ℝ)
Theorem	dvfsumlem1 23789*	Lemma for dvfsumrlim 23794. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑈)    &   ⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1))    ⇒   ⊢ (𝜑 → (𝐻‘𝑌) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
Theorem	dvfsumlem2 23790*	Lemma for dvfsumrlim 23794. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑈)    &   ⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1))    ⇒   ⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵)))
Theorem	dvfsumlem3 23791*	Lemma for dvfsumrlim 23794. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵)))
Theorem	dvfsumlem4 23792*	Lemma for dvfsumrlim 23794. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈)) → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑈)    ⇒   ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐵)
Theorem	dvfsumrlimge0 23793*	Lemma for dvfsumrlim 23794. Satisfy the assumption of dvfsumlem4 23792. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵)
Theorem	dvfsumrlim 23794*	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 23795*	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 23796*	Conjoin the statements of dvfsumrlim 23794 and dvfsumrlim2 23795. (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 23797*	The reverse of dvfsumrlim 23794, 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 23798*	Lemma for ftc1a 23800 and ftc1 23805. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡)
Theorem	ftc1lem2 23799*	Lemma for ftc1 23805. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    ⇒   ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ)
Theorem	ftc1a 23800*	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→ℂ))