Home | Metamath
Proof Explorer Theorem List (p. 194 of 315) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21491) |
Hilbert Space Explorer
(21492-23014) |
Users' Mathboxes
(23015-31422) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvmptid 19301* | Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | dvmptc 19302* | Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | dvmptcl 19303* | Closure lemma for dvmptcmul 19308 and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | dvmptadd 19304* | Function-builder for derivative, addition rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | dvmptmul 19305* | Function-builder for derivative, product rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | dvmptres2 19306* | Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
↾_{t} ℂ_{fld} | ||
Theorem | dvmptres 19307* | 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.) |
↾_{t} ℂ_{fld} | ||
Theorem | dvmptcmul 19308* | Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | dvmptdivc 19309* | Function-builder for derivative, division rule for constant divisor. (Contributed by Mario Carneiro, 18-May-2016.) |
Theorem | dvmptneg 19310* | Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | dvmptsub 19311* | Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | dvmptcj 19312* | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | dvmptre 19313* | Function-builder for derivative, real part. (Contributed by Mario Carneiro, 1-Sep-2014.) |
Theorem | dvmptim 19314* | Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014.) |
Theorem | dvmptntr 19315* | 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} ℂ_{fld} | ||
Theorem | dvmptco 19316* | Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.) |
Theorem | dvmptfsum 19317* | Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
↾_{t} ℂ_{fld} | ||
Theorem | dvcnvlem 19318 | Lemma for dvcnvre 19361. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
ℂ_{fld} ↾_{t} | ||
Theorem | dvcnv 19319* | A weak version of dvcnvre 19361, 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.) |
ℂ_{fld} ↾_{t} | ||
Theorem | dvexp3 19320* | Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | dveflem 19321 | Derivative of the exponential function at 0. The key step in the proof is eftlub 12384, to show that . (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
Theorem | dvef 19322 | Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.) |
Theorem | dvsincos 19323 | Derivative of the sine and cosine functions. (Contributed by Mario Carneiro, 21-May-2016.) |
Theorem | dvsin 19324 | Derivative of the sine function. (Contributed by Mario Carneiro, 21-May-2016.) |
Theorem | dvcos 19325 | Derivative of the cosine function. (Contributed by Mario Carneiro, 21-May-2016.) |
Theorem | dvferm1lem 19326* | Lemma for dvferm 19330. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | dvferm1 19327* | One-sided version of dvferm 19330. 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.) |
Theorem | dvferm2lem 19328* | Lemma for dvferm 19330. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | dvferm2 19329* | One-sided version of dvferm 19330. 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.) |
Theorem | dvferm 19330* | 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.) |
Theorem | rollelem 19331* | Lemma for rolle 19332. (Contributed by Mario Carneiro, 1-Sep-2014.) |
Theorem | rolle 19332* | Rolle's theorem. If is a real continuous function on which is differentiable on , and , then there is some such that . (Contributed by Mario Carneiro, 1-Sep-2014.) |
Theorem | cmvth 19333* | 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.) |
Theorem | mvth 19334* | The Mean Value Theorem. If is a real continuous function on which is differentiable on , then there is some such that is equal to the average slope over . (Contributed by Mario Carneiro, 1-Sep-2014.) (Proof shortened by Mario Carneiro, 29-Dec-2016.) |
Theorem | dvlip 19335* | A function with derivative bounded by is Lipschitz continuous with Lipchitz constant equal to . (Contributed by Mario Carneiro, 3-Mar-2015.) |
Theorem | dvlipcn 19336* | A complex function with derivative bounded by on an open ball is Lipschitz continuous with Lipchitz constant equal to . (Contributed by Mario Carneiro, 18-Mar-2015.) |
Theorem | dvlip2 19337* | Combine the results of dvlip 19335 and dvlipcn 19336 into one. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
Theorem | c1liplem1 19338* | Lemma for c1lip1 19339. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
Theorem | c1lip1 19339* | C1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
Theorem | c1lip2 19340* | C1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
Theorem | c1lip3 19341* | C1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
Theorem | dveq0 19342 | 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.) |
Theorem | dv11cn 19343 | 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.) |
Theorem | dvgt0lem1 19344 | Lemma for dvgt0 19346 and dvlt0 19347. (Contributed by Mario Carneiro, 19-Feb-2015.) |
Theorem | dvgt0lem2 19345* | Lemma for dvgt0 19346 and dvlt0 19347. (Contributed by Mario Carneiro, 19-Feb-2015.) |
Theorem | dvgt0 19346 | A function on a closed interval with positive derivative is increasing. (Contributed by Mario Carneiro, 19-Feb-2015.) |
Theorem | dvlt0 19347 | A function on a closed interval with negative derivative is decreasing. (Contributed by Mario Carneiro, 19-Feb-2015.) |
Theorem | dvge0 19348 | A function on a closed interval with nonnegative derivative is weakly increasing. (Contributed by Mario Carneiro, 30-Apr-2016.) |
Theorem | dvle 19349* | If are differentiable functions and , then for , . (Contributed by Mario Carneiro, 16-May-2016.) |
Theorem | dvivthlem1 19350* | Lemma for dvivth 19352. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | dvivthlem2 19351* | Lemma for dvivth 19352. (Contributed by Mario Carneiro, 20-Feb-2015.) |
Theorem | dvivth 19352 | 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 18813 does not directly apply). (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | dvne0 19353 | A function on a closed interval with nonzero derivative is either monotone increasing or monotone decreasing. (Contributed by Mario Carneiro, 19-Feb-2015.) |
Theorem | dvne0f1 19354 | A function on a closed interval with nonzero derivative is one-to-one. (Contributed by Mario Carneiro, 19-Feb-2015.) |
Theorem | lhop1lem 19355* | Lemma for lhop1 19356. (Contributed by Mario Carneiro, 29-Dec-2016.) |
lim lim lim | ||
Theorem | lhop1 19356* | 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.) |
lim lim lim lim | ||
Theorem | lhop2 19357* | 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.) |
lim lim lim lim | ||
Theorem | lhop 19358* | 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 . (Contributed by Mario Carneiro, 30-Dec-2016.) |
lim lim lim lim | ||
Theorem | dvcnvrelem1 19359 | Lemma for dvcnvre 19361. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | dvcnvrelem2 19360 | Lemma for dvcnvre 19361. (Contributed by Mario Carneiro, 19-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
ℂ_{fld} ↾_{t} ↾_{t} | ||
Theorem | dvcnvre 19361* | The derivative rule for inverse functions. If is a continuous and differentiable bijective function from to which never has derivative , then is also differentiable, and its derivative is the reciprocal of the derivative of . (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | dvcvx 19362 | A real function with strictly increasing derivative is strictly convex. (Contributed by Mario Carneiro, 20-Jun-2015.) |
Theorem | dvfsumle 19363* | 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.) |
..^ ..^ ..^ | ||
Theorem | dvfsumge 19364* | 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.) |
..^ ..^ ..^ | ||
Theorem | dvfsumabs 19365* | 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.) |
..^ ..^ ..^ ..^ ..^ | ||
Theorem | dvmptrecl 19366* | Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016.) |
Theorem | dvfsumrlimf 19367* | Lemma for dvfsumrlim 19373. (Contributed by Mario Carneiro, 18-May-2016.) |
Theorem | dvfsumlem1 19368* | Lemma for dvfsumrlim 19373. (Contributed by Mario Carneiro, 17-May-2016.) |
Theorem | dvfsumlem2 19369* | Lemma for dvfsumrlim 19373. (Contributed by Mario Carneiro, 17-May-2016.) |
Theorem | dvfsumlem3 19370* | Lemma for dvfsumrlim 19373. (Contributed by Mario Carneiro, 17-May-2016.) |
Theorem | dvfsumlem4 19371* | Lemma for dvfsumrlim 19373. (Contributed by Mario Carneiro, 18-May-2016.) |
Theorem | dvfsumrlimge0 19372* | Lemma for dvfsumrlim 19373. Satisfy the assumption of dvfsumlem4 19371. (Contributed by Mario Carneiro, 18-May-2016.) |
Theorem | dvfsumrlim 19373* | 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 converges to a constant limit value, with the remainder term bounded by . (Contributed by Mario Carneiro, 18-May-2016.) |
Theorem | dvfsumrlim2 19374* | 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 converges to a constant limit value, with the remainder term bounded by . (Contributed by Mario Carneiro, 18-May-2016.) |
Theorem | dvfsumrlim3 19375* | Conjoin the statements of dvfsumrlim 19373 and dvfsumrlim2 19374. (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.) |
Theorem | dvfsum2 19376* | The reverse of dvfsumrlim 19373, 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.) |
Theorem | ftc1lem1 19377* | Lemma for ftc1a 19379 and ftc1 19384. (Contributed by Mario Carneiro, 31-Aug-2014.) |
Theorem | ftc1lem2 19378* | Lemma for ftc1 19384. (Contributed by Mario Carneiro, 12-Aug-2014.) |
Theorem | ftc1a 19379* | 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.) |
Theorem | ftc1lem3 19380* | Lemma for ftc1 19384. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 8-Sep-2015.) |
↾_{t} ↾_{t} ℂ_{fld} | ||
Theorem | ftc1lem4 19381* | Lemma for ftc1 19384. (Contributed by Mario Carneiro, 31-Aug-2014.) |
↾_{t} ↾_{t} ℂ_{fld} | ||
Theorem | ftc1lem5 19382* | Lemma for ftc1 19384. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
↾_{t} ↾_{t} ℂ_{fld} | ||
Theorem | ftc1lem6 19383* | Lemma for ftc1 19384. (Contributed by Mario Carneiro, 14-Aug-2014.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
↾_{t} ↾_{t} ℂ_{fld} lim | ||
Theorem | ftc1 19384* | 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 . (Contributed by Mario Carneiro, 1-Sep-2014.) |
↾_{t} ↾_{t} ℂ_{fld} | ||
Theorem | ftc1cn 19385* | Strengthen the assumptions of ftc1 19384 to when the function is continuous on the entire interval ; in this case we can calculate exactly. (Contributed by Mario Carneiro, 1-Sep-2014.) |
Theorem | ftc2 19386* | 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 . (Contributed by Mario Carneiro, 2-Sep-2014.) |
Theorem | ftc2ditglem 19387* | Lemma for ftc2ditg 19388. (Contributed by Mario Carneiro, 3-Sep-2014.) |
_ | ||
Theorem | ftc2ditg 19388* | Directed integral analog of ftc2 19386. (Contributed by Mario Carneiro, 3-Sep-2014.) |
_ | ||
Theorem | itgparts 19389* | 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.) |
Theorem | itgsubstlem 19390* | Lemma for itgsubst 19391. (Contributed by Mario Carneiro, 12-Sep-2014.) |
_ _ | ||
Theorem | itgsubst 19391* | 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 from to . In this part of the proof we discharge the assumptions in itgsubstlem 19390, 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.) |
_ _ | ||
Theorem | evlslem6 19392* | Lemma for evlseu 19395. Finiteness and consistency of the top level sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
mPoly mulGrp ._{g} mVar _{g} _{g} RingHom _{g} _{g} | ||
Theorem | evlslem3 19393* | Lemma for evlseu 19395. Polynomial evaluation of a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
mPoly mulGrp ._{g} mVar _{g} _{g} RingHom _{g} | ||
Theorem | evlslem1 19394* | Lemma for evlseu 19395, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
mPoly mulGrp ._{g} mVar _{g} _{g} RingHom algSc RingHom | ||
Theorem | evlseu 19395* | For a given intepretation of the variables and of the scalars , this extends to a homomorphic interpretation of the polynomial ring in exactly one way. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
mPoly algSc mVar RingHom RingHom | ||
Theorem | reldmevls 19396 | Well-behaved binary operation property of evalSub. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
evalSub | ||
Theorem | mpfrcl 19397 | Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
evalSub SubRing | ||
Theorem | evlsval 19398* | Value of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
evalSub mPoly mVar ↾_{s} _{s} algSc SubRing RingHom | ||
Theorem | evlsval2 19399* | Characterizing properties of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 12-Mar-2015.) |
evalSub mPoly mVar ↾_{s} _{s} algSc SubRing RingHom | ||
Theorem | evlsrhm 19400 | Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Stefan O'Rear, 12-Mar-2015.) |
evalSub mPoly ↾_{s} _{s} SubRing RingHom |
< Previous Next > |