| Metamath
Proof Explorer Theorem List (p. 261 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dvmptres 26001* | 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 26002* | 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 26003* | Function-builder for derivative, division rule for constant divisor. (Contributed by Mario Carneiro, 18-May-2016.) |
| ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶))) | ||
| Theorem | dvmptneg 26004* | 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 26005* | 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 26006* | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (∗‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (∗‘𝐵))) | ||
| Theorem | dvmptre 26007* | Function-builder for derivative, real part. (Contributed by Mario Carneiro, 1-Sep-2014.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℜ‘𝐵))) | ||
| Theorem | dvmptim 26008* | Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐴))) = (𝑥 ∈ 𝑋 ↦ (ℑ‘𝐵))) | ||
| Theorem | dvmptntr 26009* | 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 26010* | Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.) |
| ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → (𝑇 D (𝑦 ∈ 𝑌 ↦ 𝐶)) = (𝑦 ∈ 𝑌 ↦ 𝐷)) & ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐸) & ⊢ (𝑦 = 𝐴 → 𝐷 = 𝐹) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐸)) = (𝑥 ∈ 𝑋 ↦ (𝐹 · 𝐵))) | ||
| Theorem | dvrecg 26011* | Derivative of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐵)) = (𝑥 ∈ 𝑋 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵))) = (𝑥 ∈ 𝑋 ↦ -((𝐴 · 𝐶) / (𝐵↑2)))) | ||
| Theorem | dvmptdiv 26012* | Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ ℂ) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (((𝐵 · 𝐶) − (𝐷 · 𝐴)) / (𝐶↑2)))) | ||
| Theorem | dvmptfsum 26013* | Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
| ⊢ 𝐽 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵)) | ||
| Theorem | dvcnvlem 26014 | Lemma for dvcnvre 26058. (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 26015* | A weak version of dvcnvre 26058, 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 26016* | Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015.) |
| ⊢ (𝑁 ∈ ℤ → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥↑𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) | ||
| Theorem | dveflem 26017 | Derivative of the exponential function at 0. The key step in the proof is eftlub 16145, 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 26018 | 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 26019 | Derivative of the sine and cosine functions. (Contributed by Mario Carneiro, 21-May-2016.) |
| ⊢ ((ℂ D sin) = cos ∧ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥))) | ||
| Theorem | dvsin 26020 | Derivative of the sine function. (Contributed by Mario Carneiro, 21-May-2016.) |
| ⊢ (ℂ D sin) = cos | ||
| Theorem | dvcos 26021 | Derivative of the cosine function. (Contributed by Mario Carneiro, 21-May-2016.) |
| ⊢ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥)) | ||
| Theorem | dvferm1lem 26022* | Lemma for dvferm 26026. (Contributed by Mario Carneiro, 24-Feb-2015.) |
| ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) & ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) & ⊢ (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) & ⊢ (𝜑 → 0 < ((ℝ D 𝐹)‘𝑈)) & ⊢ (𝜑 → 𝑇 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) & ⊢ 𝑆 = ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | dvferm1 26023* | One-sided version of dvferm 26026. 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 26024* | Lemma for dvferm 26026. (Contributed by Mario Carneiro, 24-Feb-2015.) |
| ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) & ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) & ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) & ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) < 0) & ⊢ (𝜑 → 𝑇 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) & ⊢ 𝑆 = ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | dvferm2 26025* | One-sided version of dvferm 26026. 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 26026* | 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 26027* | Lemma for rolle 26028. (Contributed by Mario Carneiro, 1-Sep-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) & ⊢ (𝜑 → 𝑈 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → ¬ 𝑈 ∈ {𝐴, 𝐵}) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) | ||
| Theorem | rolle 26028* | 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 26029* | 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 11235. (Revised by GG, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) | ||
| Theorem | cmvthOLD 26030* | Obsolete version of cmvth 26029 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 26031* | 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 26032* | 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 26033* | 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 26034* | Combine the results of dvlip 26032 and dvlipcn 26033 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 26035* | Lemma for c1lip1 26036. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm ℝ)) & ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ 𝐾 = sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < ) ⇒ ⊢ (𝜑 → (𝐾 ∈ ℝ ∧ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥)))))) | ||
| Theorem | c1lip1 26036* | 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 26037* | 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 26038* | C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐹 ↾ ℝ) ∈ ((𝓑C𝑛‘ℝ)‘1)) & ⊢ (𝜑 → (𝐹 “ ℝ) ⊆ ℝ) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom 𝐹) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑘 · (abs‘(𝑦 − 𝑥)))) | ||
| Theorem | dveq0 26039 | 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 26040 | 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 26041 | Lemma for dvgt0 26043 and dvlt0 26044. (Contributed by Mario Carneiro, 19-Feb-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶𝑆) ⇒ ⊢ (((𝜑 ∧ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵))) ∧ 𝑋 < 𝑌) → (((𝐹‘𝑌) − (𝐹‘𝑋)) / (𝑌 − 𝑋)) ∈ 𝑆) | ||
| Theorem | dvgt0lem2 26042* | Lemma for dvgt0 26043 and dvlt0 26044. (Contributed by Mario Carneiro, 19-Feb-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶𝑆) & ⊢ 𝑂 Or ℝ & ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹‘𝑥)𝑂(𝐹‘𝑦)) ⇒ ⊢ (𝜑 → 𝐹 Isom < , 𝑂 ((𝐴[,]𝐵), ran 𝐹)) | ||
| Theorem | dvgt0 26043 | A function on a closed interval with positive derivative is increasing. (Contributed by Mario Carneiro, 19-Feb-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ+) ⇒ ⊢ (𝜑 → 𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹)) | ||
| Theorem | dvlt0 26044 | 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 26045 | A function on a closed interval with nonnegative derivative is weakly increasing. (Contributed by Mario Carneiro, 30-Apr-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ≤ (𝐹‘𝑌)) | ||
| Theorem | dvle 26046* | If 𝐴(𝑥), 𝐶(𝑥) are differentiable functions and 𝐴‘ ≤ 𝐶‘, then for 𝑥 ≤ 𝑦, 𝐴(𝑦) − 𝐴(𝑥) ≤ 𝐶(𝑦) − 𝐶(𝑥). (Contributed by Mario Carneiro, 16-May-2016.) |
| ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) & ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ≤ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑀[,]𝑁)) & ⊢ (𝜑 → 𝑌 ∈ (𝑀[,]𝑁)) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝑥 = 𝑋 → 𝐴 = 𝑃) & ⊢ (𝑥 = 𝑋 → 𝐶 = 𝑄) & ⊢ (𝑥 = 𝑌 → 𝐴 = 𝑅) & ⊢ (𝑥 = 𝑌 → 𝐶 = 𝑆) ⇒ ⊢ (𝜑 → (𝑅 − 𝑃) ≤ (𝑆 − 𝑄)) | ||
| Theorem | dvivthlem1 26047* | Lemma for dvivth 26049. (Contributed by Mario Carneiro, 24-Feb-2015.) |
| ⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝑀 < 𝑁) & ⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀))) & ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶) | ||
| Theorem | dvivthlem2 26048* | Lemma for dvivth 26049. (Contributed by Mario Carneiro, 20-Feb-2015.) |
| ⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝑀 < 𝑁) & ⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀))) & ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦))) ⇒ ⊢ (𝜑 → 𝐶 ∈ ran (ℝ D 𝐹)) | ||
| Theorem | dvivth 26049 | 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 25493 does not directly apply). (Contributed by Mario Carneiro, 24-Feb-2015.) |
| ⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) ⇒ ⊢ (𝜑 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) | ||
| Theorem | dvne0 26050 | 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 26051 | 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 26052* | Lemma for lhop1 26053. (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 26053* | 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 26054* | 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 26055* | 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 26056 | Lemma for dvcnvre 26058. (Contributed by Mario Carneiro, 24-Feb-2015.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋) & ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹)) & ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) | ||
| Theorem | dvcnvrelem2 26057 | Lemma for dvcnvre 26058. (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 26058* | 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 26059 | 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 26060* | 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 11235. (Revised by GG, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) & ⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝑋 ≤ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ (𝐷 − 𝐶)) | ||
| Theorem | dvfsumleOLD 26061* | Obsolete version of dvfsumle 26060 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 26062* | 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 26063* | 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 26064* | Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016.) |
| ⊢ (𝜑 → 𝑆 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) | ||
| Theorem | dvfsumrlimf 26065* | Lemma for dvfsumrlim 26072. (Contributed by Mario Carneiro, 18-May-2016.) |
| ⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) ⇒ ⊢ (𝜑 → 𝐺:𝑆⟶ℝ) | ||
| Theorem | dvfsumlem1 26066* | Lemma for dvfsumrlim 26072. (Contributed by Mario Carneiro, 17-May-2016.) |
| ⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝑈 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) & ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ≤ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑈) & ⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1)) ⇒ ⊢ (𝜑 → (𝐻‘𝑌) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) | ||
| Theorem | dvfsumlem2 26067* | Lemma for dvfsumrlim 26072. (Contributed by Mario Carneiro, 17-May-2016.) Avoid ax-mulf 11235. (Revised by GG, 16-Mar-2025.) |
| ⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝑈 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) & ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ≤ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑈) & ⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1)) ⇒ ⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵))) | ||
| Theorem | dvfsumlem2OLD 26068* | Obsolete version of dvfsumlem2 26067 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 26069* | Lemma for dvfsumrlim 26072. (Contributed by Mario Carneiro, 17-May-2016.) |
| ⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝑈 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) & ⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ≤ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑈) ⇒ ⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵))) | ||
| Theorem | dvfsumlem4 26070* | Lemma for dvfsumrlim 26072. (Contributed by Mario Carneiro, 18-May-2016.) |
| ⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝑈 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈)) → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ≤ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑈) ⇒ ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐵) | ||
| Theorem | dvfsumrlimge0 26071* | Lemma for dvfsumrlim 26072. Satisfy the assumption of dvfsumlem4 26070. (Contributed by Mario Carneiro, 18-May-2016.) |
| ⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) & ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵) | ||
| Theorem | dvfsumrlim 26072* | 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 26073* | 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 26074* | Conjoin the statements of dvfsumrlim 26072 and dvfsumrlim2 26073. (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 26075* | The reverse of dvfsumrlim 26072, 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 26076* | Lemma for ftc1a 26078 and ftc1 26083. (Contributed by Mario Carneiro, 31-Aug-2014.) |
| ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡) | ||
| Theorem | ftc1lem2 26077* | Lemma for ftc1 26083. (Contributed by Mario Carneiro, 12-Aug-2014.) |
| ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) | ||
| Theorem | ftc1a 26078* | 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 26079* | Lemma for ftc1 26083. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 8-Sep-2015.) |
| ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) & ⊢ 𝐽 = (𝐿 ↾t ℝ) & ⊢ 𝐾 = (𝐿 ↾t 𝐷) & ⊢ 𝐿 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) | ||
| Theorem | ftc1lem4 26080* | Lemma for ftc1 26083. (Contributed by Mario Carneiro, 31-Aug-2014.) |
| ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) & ⊢ 𝐽 = (𝐿 ↾t ℝ) & ⊢ 𝐾 = (𝐿 ↾t 𝐷) & ⊢ 𝐿 = (TopOpen‘ℂfld) & ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((abs‘(𝑦 − 𝐶)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) < 𝑅) & ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑌 − 𝐶)) < 𝑅) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝐶))) < 𝐸) | ||
| Theorem | ftc1lem5 26081* | Lemma for ftc1 26083. (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 26082* | Lemma for ftc1 26083. (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 26083* | 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 26084* | Strengthen the assumptions of ftc1 26083 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 26085* | 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 26086* | Lemma for ftc2ditg 26087. (Contributed by Mario Carneiro, 3-Sep-2014.) |
| ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1) & ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) | ||
| Theorem | ftc2ditg 26087* | Directed integral analogue of ftc2 26085. (Contributed by Mario Carneiro, 3-Sep-2014.) |
| ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1) & ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ)) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) | ||
| Theorem | itgparts 26088* | 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 26089* | Lemma for itgsubst 26090. (Contributed by Mario Carneiro, 12-Sep-2014.) |
| ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ ℝ*) & ⊢ (𝜑 → 𝑊 ∈ ℝ*) & ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1)) & ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) & ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸) & ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾) & ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿) & ⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊)) & ⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁)) ⇒ ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥) | ||
| Theorem | itgsubst 26090* | 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 26089, 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 26091* | 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))) | ||
| Syntax | cmdg 26092 | Multivariate polynomial degree. |
| class mDeg | ||
| Syntax | cdg1 26093 | Univariate polynomial degree. |
| class deg1 | ||
| Definition | df-mdeg 26094* | 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 26230. (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 26095 | Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ deg1 = (𝑟 ∈ V ↦ (1o mDeg 𝑟)) | ||
| Theorem | reldmmdeg 26096 | Multivariate degree is a binary operation. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ Rel dom mDeg | ||
| Theorem | tdeglem1 26097* | 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 26098* | 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 26099* | 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 26100 | Simplification of total degree for the univariate case. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ (ℎ ∈ (ℕ0 ↑m 1o) ↦ (ℎ‘∅)) = (ℎ ∈ (ℕ0 ↑m 1o) ↦ (ℂfld Σg ℎ)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |