![]() |
Metamath
Proof Explorer Theorem List (p. 261 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvcjbr 26001 | The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 26002. (This doesn't follow from dvcobr 25997 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 26002 | The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 26001. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → (ℝ D (∗ ∘ 𝐹)) = (∗ ∘ (ℝ D 𝐹))) | ||
Theorem | dvfre 26003 | The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) | ||
Theorem | dvnfre 26004 | The 𝑁-th derivative of a real function is real. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑁 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑁):dom ((ℝ D𝑛 𝐹)‘𝑁)⟶ℝ) | ||
Theorem | dvexp 26005* | Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
⊢ (𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) | ||
Theorem | dvexp2 26006* | 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 26007* | 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 26008* | Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ (𝜑 → (𝑆 ∩ 𝑋) = 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑌 ↦ 𝐵)) | ||
Theorem | dvmptid 26009* | 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 26010* | 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 26011* | Closure lemma for dvmptcmul 26016 and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ) | ||
Theorem | dvmptadd 26012* | 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 26013* | 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 26014* | 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 26015* | 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 26016* | 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 26017* | Function-builder for derivative, division rule for constant divisor. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶))) | ||
Theorem | dvmptneg 26018* | 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 26019* | 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 26020* | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (∗‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (∗‘𝐵))) | ||
Theorem | dvmptre 26021* | Function-builder for derivative, real part. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐵))) | ||
Theorem | dvmptim 26022* | Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐵))) | ||
Theorem | dvmptntr 26023* | 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 26024* | Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷)) & ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸) & ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵))) | ||
Theorem | dvrecg 26025* | Derivative of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐵)) = (𝑥 ∈ 𝑋 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵))) = (𝑥 ∈ 𝑋 ↦ -((𝐴 · 𝐶) / (𝐵↑2)))) | ||
Theorem | dvmptdiv 26026* | Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ ℂ) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (((𝐵 · 𝐶) − (𝐷 · 𝐴)) / (𝐶↑2)))) | ||
Theorem | dvmptfsum 26027* | Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
⊢ 𝐽 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵)) | ||
Theorem | dvcnvlem 26028 | Lemma for dvcnvre 26072. (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 26029* | A weak version of dvcnvre 26072, 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 26030* | Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝑁 ∈ ℤ → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥↑𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) | ||
Theorem | dveflem 26031 | Derivative of the exponential function at 0. The key step in the proof is eftlub 16141, 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 26032 | 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 26033 | Derivative of the sine and cosine functions. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ ((ℂ D sin) = cos ∧ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥))) | ||
Theorem | dvsin 26034 | Derivative of the sine function. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ (ℂ D sin) = cos | ||
Theorem | dvcos 26035 | Derivative of the cosine function. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥)) | ||
Theorem | dvferm1lem 26036* | Lemma for dvferm 26040. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) & ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) & ⊢ (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) & ⊢ (𝜑 → 0 < ((ℝ D 𝐹)‘𝑈)) & ⊢ (𝜑 → 𝑇 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) & ⊢ 𝑆 = ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | dvferm1 26037* | One-sided version of dvferm 26040. 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 26038* | Lemma for dvferm 26040. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) & ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) & ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) & ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) < 0) & ⊢ (𝜑 → 𝑇 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) & ⊢ 𝑆 = ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | dvferm2 26039* | One-sided version of dvferm 26040. 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 26040* | 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 26041* | Lemma for rolle 26042. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) & ⊢ (𝜑 → 𝑈 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → ¬ 𝑈 ∈ {𝐴, 𝐵}) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) | ||
Theorem | rolle 26042* | 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 26043* | 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 11232. (Revised by GG, 16-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) | ||
Theorem | cmvthOLD 26044* | Obsolete version of cmvth 26043 as of 16-Apr-2025. (Contributed by Mario Carneiro, 29-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) | ||
Theorem | mvth 26045* | 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 26046* | 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 26047* | 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 26048* | Combine the results of dvlip 26046 and dvlipcn 26047 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 26049* | Lemma for c1lip1 26050. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm ℝ)) & ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ 𝐾 = sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < ) ⇒ ⊢ (𝜑 → (𝐾 ∈ ℝ ∧ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥)))))) | ||
Theorem | c1lip1 26050* | 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 26051* | 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 26052* | C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐹 ↾ ℝ) ∈ ((𝓑C𝑛‘ℝ)‘1)) & ⊢ (𝜑 → (𝐹 “ ℝ) ⊆ ℝ) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom 𝐹) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑘 · (abs‘(𝑦 − 𝑥)))) | ||
Theorem | dveq0 26053 | 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 26054 | 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 26055 | Lemma for dvgt0 26057 and dvlt0 26058. (Contributed by Mario Carneiro, 19-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶𝑆) ⇒ ⊢ (((𝜑 ∧ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵))) ∧ 𝑋 < 𝑌) → (((𝐹‘𝑌) − (𝐹‘𝑋)) / (𝑌 − 𝑋)) ∈ 𝑆) | ||
Theorem | dvgt0lem2 26056* | Lemma for dvgt0 26057 and dvlt0 26058. (Contributed by Mario Carneiro, 19-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶𝑆) & ⊢ 𝑂 Or ℝ & ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹‘𝑥)𝑂(𝐹‘𝑦)) ⇒ ⊢ (𝜑 → 𝐹 Isom < , 𝑂 ((𝐴[,]𝐵), ran 𝐹)) | ||
Theorem | dvgt0 26057 | A function on a closed interval with positive derivative is increasing. (Contributed by Mario Carneiro, 19-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ+) ⇒ ⊢ (𝜑 → 𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹)) | ||
Theorem | dvlt0 26058 | 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 26059 | A function on a closed interval with nonnegative derivative is weakly increasing. (Contributed by Mario Carneiro, 30-Apr-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ≤ (𝐹‘𝑌)) | ||
Theorem | dvle 26060* | If 𝐴(𝑥), 𝐶(𝑥) are differentiable functions and 𝐴‘ ≤ 𝐶‘, then for 𝑥 ≤ 𝑦, 𝐴(𝑦) − 𝐴(𝑥) ≤ 𝐶(𝑦) − 𝐶(𝑥). (Contributed by Mario Carneiro, 16-May-2016.) |
⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) & ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ≤ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑀[,]𝑁)) & ⊢ (𝜑 → 𝑌 ∈ (𝑀[,]𝑁)) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝑥 = 𝑋 → 𝐴 = 𝑃) & ⊢ (𝑥 = 𝑋 → 𝐶 = 𝑄) & ⊢ (𝑥 = 𝑌 → 𝐴 = 𝑅) & ⊢ (𝑥 = 𝑌 → 𝐶 = 𝑆) ⇒ ⊢ (𝜑 → (𝑅 − 𝑃) ≤ (𝑆 − 𝑄)) | ||
Theorem | dvivthlem1 26061* | Lemma for dvivth 26063. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝑀 < 𝑁) & ⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀))) & ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶) | ||
Theorem | dvivthlem2 26062* | Lemma for dvivth 26063. (Contributed by Mario Carneiro, 20-Feb-2015.) |
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝑀 < 𝑁) & ⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀))) & ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦))) ⇒ ⊢ (𝜑 → 𝐶 ∈ ran (ℝ D 𝐹)) | ||
Theorem | dvivth 26063 | 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 25506 does not directly apply). (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) ⇒ ⊢ (𝜑 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) | ||
Theorem | dvne0 26064 | 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 26065 | 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 26066* | Lemma for lhop1 26067. (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 26067* | 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 26068* | 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 26069* | 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 26070 | Lemma for dvcnvre 26072. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋) & ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹)) & ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) | ||
Theorem | dvcnvrelem2 26071 | Lemma for dvcnvre 26072. (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 26072* | 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 26073 | 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 26074* | 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 11232. (Revised by GG, 16-Mar-2025.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) & ⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝑋 ≤ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ (𝐷 − 𝐶)) | ||
Theorem | dvfsumleOLD 26075* | Obsolete version of dvfsumle 26074 as of 17-Apr-2025. (Contributed by Mario Carneiro, 14-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) & ⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝑋 ≤ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ (𝐷 − 𝐶)) | ||
Theorem | dvfsumge 26076* | 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 26077* | 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 26078* | Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ (𝜑 → 𝑆 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) | ||
Theorem | dvfsumrlimf 26079* | Lemma for dvfsumrlim 26086. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) ⇒ ⊢ (𝜑 → 𝐺:𝑆⟶ℝ) | ||
Theorem | dvfsumlem1 26080* | Lemma for dvfsumrlim 26086. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝑈 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) & ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ≤ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑈) & ⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1)) ⇒ ⊢ (𝜑 → (𝐻‘𝑌) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) | ||
Theorem | dvfsumlem2 26081* | Lemma for dvfsumrlim 26086. (Contributed by Mario Carneiro, 17-May-2016.) Avoid ax-mulf 11232. (Revised by GG, 16-Mar-2025.) |
⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝑈 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) & ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ≤ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑈) & ⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1)) ⇒ ⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵))) | ||
Theorem | dvfsumlem2OLD 26082* | Obsolete version of dvfsumlem2 26081 as of 17-Apr-2025. (Contributed by Mario Carneiro, 17-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝑈 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) & ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ≤ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑈) & ⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1)) ⇒ ⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵))) | ||
Theorem | dvfsumlem3 26083* | Lemma for dvfsumrlim 26086. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝑈 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) & ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ≤ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑈) ⇒ ⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵))) | ||
Theorem | dvfsumlem4 26084* | Lemma for dvfsumrlim 26086. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝑈 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈)) → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ≤ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑈) ⇒ ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐵) | ||
Theorem | dvfsumrlimge0 26085* | Lemma for dvfsumrlim 26086. Satisfy the assumption of dvfsumlem4 26084. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) & ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵) | ||
Theorem | dvfsumrlim 26086* | 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 26087* | 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 26088* | Conjoin the statements of dvfsumrlim 26086 and dvfsumrlim2 26087. (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 26089* | The reverse of dvfsumrlim 26086, 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 26090* | Lemma for ftc1a 26092 and ftc1 26097. (Contributed by Mario Carneiro, 31-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡) | ||
Theorem | ftc1lem2 26091* | Lemma for ftc1 26097. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) | ||
Theorem | ftc1a 26092* | 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 26093* | Lemma for ftc1 26097. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) & ⊢ 𝐽 = (𝐿 ↾t ℝ) & ⊢ 𝐾 = (𝐿 ↾t 𝐷) & ⊢ 𝐿 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) | ||
Theorem | ftc1lem4 26094* | Lemma for ftc1 26097. (Contributed by Mario Carneiro, 31-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) & ⊢ 𝐽 = (𝐿 ↾t ℝ) & ⊢ 𝐾 = (𝐿 ↾t 𝐷) & ⊢ 𝐿 = (TopOpen‘ℂfld) & ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((abs‘(𝑦 − 𝐶)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) < 𝑅) & ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑌 − 𝐶)) < 𝑅) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝐶))) < 𝐸) | ||
Theorem | ftc1lem5 26095* | Lemma for ftc1 26097. (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 26096* | Lemma for ftc1 26097. (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 26097* | 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 26098* | Strengthen the assumptions of ftc1 26097 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 26099* | 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 26100* | Lemma for ftc2ditg 26101. (Contributed by Mario Carneiro, 3-Sep-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1) & ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |