P. 230 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22901-23000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvcjbr 22901	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 22902. (This doesn't follow from dvcobr 22898 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.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ RR )   &    |- ( ph -> C e. dom ( RR _D F ) )   =>    |- ( ph -> C ( RR _D ( * o. F ) ) ( * ` ( ( RR _D F ) ` C ) ) )
Theorem	dvcj 22902	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 22901. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ( F : X --> CC /\ X C_ RR ) -> ( RR _D ( * o. F ) ) = ( * o. ( RR _D F ) ) )
Theorem	dvfre 22903	The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ( F : A --> RR /\ A C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
Theorem	dvnfre 22904	The N-th derivative of a real function is real. (Contributed by Mario Carneiro, 1-Jan-2017.)
|- ( ( F : A --> RR /\ A C_ RR /\ N e. NN0 ) -> ( ( RR Dn F ) ` N ) : dom ( ( RR Dn F ) ` N ) --> RR )
Theorem	dvexp 22905*	Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( N e. NN -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )
Theorem	dvexp2 22906*	Derivative of an exponential, possibly zero power. (Contributed by Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( N e. NN0 -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) )
Theorem	dvrec 22907*	Derivative of the reciprocal function. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- ( A e. CC -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) = ( x e. ( CC \ { 0 } ) |-> -u ( A / ( x ^ 2 ) ) ) )
Theorem	dvmptres3 22908*	Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- J = ( TopOpen ` ℂfld )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. J )   &    |- ( ph -> ( S i^i X ) = Y )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( CC _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   =>    |- ( ph -> ( S _D ( x e. Y |-> A ) ) = ( x e. Y |-> B ) )
Theorem	dvmptid 22909*	Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   =>    |- ( ph -> ( S _D ( x e. S |-> x ) ) = ( x e. S |-> 1 ) )
Theorem	dvmptc 22910*	Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> A e. CC )   =>    |- ( ph -> ( S _D ( x e. S |-> A ) ) = ( x e. S |-> 0 ) )
Theorem	dvmptcl 22911*	Closure lemma for dvmptcmul 22916 and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   =>    |- ( ( ph /\ x e. X ) -> B e. CC )
Theorem	dvmptadd 22912*	Function-builder for derivative, addition rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   &    |- ( ( ph /\ x e. X ) -> C e. CC )   &    |- ( ( ph /\ x e. X ) -> D e. W )   &    |- ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )   =>    |- ( ph -> ( S _D ( x e. X |-> ( A + C ) ) ) = ( x e. X |-> ( B + D ) ) )
Theorem	dvmptmul 22913*	Function-builder for derivative, product rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   &    |- ( ( ph /\ x e. X ) -> C e. CC )   &    |- ( ( ph /\ x e. X ) -> D e. W )   &    |- ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )   =>    |- ( ph -> ( S _D ( x e. X |-> ( A x. C ) ) ) = ( x e. X |-> ( ( B x. C ) + ( D x. A ) ) ) )
Theorem	dvmptres2 22914*	Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   &    |- ( ph -> Z C_ X )   &    |- J = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   &    |- ( ph -> ( ( int ` J ) ` Z ) = Y )   =>    |- ( ph -> ( S _D ( x e. Z |-> A ) ) = ( x e. Y |-> B ) )
Theorem	dvmptres 22915*	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.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   &    |- ( ph -> Y C_ X )   &    |- J = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   &    |- ( ph -> Y e. J )   =>    |- ( ph -> ( S _D ( x e. Y |-> A ) ) = ( x e. Y |-> B ) )
Theorem	dvmptcmul 22916*	Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( S _D ( x e. X |-> ( C x. A ) ) ) = ( x e. X |-> ( C x. B ) ) )
Theorem	dvmptdivc 22917*	Function-builder for derivative, division rule for constant divisor. (Contributed by Mario Carneiro, 18-May-2016.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( S _D ( x e. X |-> ( A / C ) ) ) = ( x e. X |-> ( B / C ) ) )
Theorem	dvmptneg 22918*	Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   =>    |- ( ph -> ( S _D ( x e. X |-> -u A ) ) = ( x e. X |-> -u B ) )
Theorem	dvmptsub 22919*	Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   &    |- ( ( ph /\ x e. X ) -> C e. CC )   &    |- ( ( ph /\ x e. X ) -> D e. W )   &    |- ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )   =>    |- ( ph -> ( S _D ( x e. X |-> ( A - C ) ) ) = ( x e. X |-> ( B - D ) ) )
Theorem	dvmptcj 22920*	Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( RR _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   =>    |- ( ph -> ( RR _D ( x e. X |-> ( * ` A ) ) ) = ( x e. X |-> ( * ` B ) ) )
Theorem	dvmptre 22921*	Function-builder for derivative, real part. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( RR _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   =>    |- ( ph -> ( RR _D ( x e. X |-> ( Re ` A ) ) ) = ( x e. X |-> ( Re ` B ) ) )
Theorem	dvmptim 22922*	Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( RR _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   =>    |- ( ph -> ( RR _D ( x e. X |-> ( Im ` A ) ) ) = ( x e. X |-> ( Im ` B ) ) )
Theorem	dvmptntr 22923*	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.)
|- ( ph -> S C_ CC )   &    |- ( ph -> X C_ S )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- J = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   &    |- ( ph -> ( ( int ` J ) ` X ) = Y )   =>    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( S _D ( x e. Y |-> A ) ) )
Theorem	dvmptco 22924*	Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> T e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ( ph /\ y e. Y ) -> C e. CC )   &    |- ( ( ph /\ y e. Y ) -> D e. W )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   &    |- ( ph -> ( T _D ( y e. Y |-> C ) ) = ( y e. Y |-> D ) )   &    |- ( y = A -> C = E )   &    |- ( y = A -> D = F )   =>    |- ( ph -> ( S _D ( x e. X |-> E ) ) = ( x e. X |-> ( F x. B ) ) )
Theorem	dvmptfsum 22925*	Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014.)
|- J = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. J )   &    |- ( ph -> I e. Fin )   &    |- ( ( ph /\ i e. I /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ i e. I /\ x e. X ) -> B e. CC )   &    |- ( ( ph /\ i e. I ) -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   =>    |- ( ph -> ( S _D ( x e. X |-> sum_ i e. I A ) ) = ( x e. X |-> sum_ i e. I B ) )
Theorem	dvcnvlem 22926	Lemma for dvcnvre 22969. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t S )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> Y e. K )   &    |- ( ph -> F : X -1-1-onto-> Y )   &    |- ( ph -> `' F e. ( Y -cn-> X ) )   &    |- ( ph -> dom ( S _D F ) = X )   &    |- ( ph -> -. 0 e. ran ( S _D F ) )   &    |- ( ph -> C e. X )   =>    |- ( ph -> ( F ` C ) ( S _D `' F ) ( 1 / ( ( S _D F ) ` C ) ) )
Theorem	dvcnv 22927*	A weak version of dvcnvre 22969, 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.)
|- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t S )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> Y e. K )   &    |- ( ph -> F : X -1-1-onto-> Y )   &    |- ( ph -> `' F e. ( Y -cn-> X ) )   &    |- ( ph -> dom ( S _D F ) = X )   &    |- ( ph -> -. 0 e. ran ( S _D F ) )   =>    |- ( ph -> ( S _D `' F ) = ( x e. Y |-> ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) ) )
Theorem	dvexp3 22928*	Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- ( N e. ZZ -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( x ^ N ) ) ) = ( x e. ( CC \ { 0 } ) |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )
Theorem	dveflem 22929	Derivative of the exponential function at 0. The key step in the proof is eftlub 14162, to show that abs ( exp ( x ) - 1 - x ) <_ abs ( x ) ^ 2 x. ( 3 / 4 ). (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- 0 ( CC _D exp ) 1
Theorem	dvef 22930	Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
|- ( CC _D exp ) = exp
Theorem	dvsincos 22931	Derivative of the sine and cosine functions. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( ( CC _D sin ) = cos /\ ( CC _D cos ) = ( x e. CC |-> -u ( sin ` x ) ) )
Theorem	dvsin 22932	Derivative of the sine function. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( CC _D sin ) = cos
Theorem	dvcos 22933	Derivative of the cosine function. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( CC _D cos ) = ( x e. CC |-> -u ( sin ` x ) )
13.3.1.2  Results on real differentiation
Theorem	dvferm1lem 22934*	Lemma for dvferm 22938. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : X --> RR )   &    |- ( ph -> X C_ RR )   &    |- ( ph -> U e. ( A (,) B ) )   &    |- ( ph -> ( A (,) B ) C_ X )   &    |- ( ph -> U e. dom ( RR _D F ) )   &    |- ( ph -> A. y e. ( U (,) B ) ( F ` y ) <_ ( F ` U ) )   &    |- ( ph -> 0 < ( ( RR _D F ) ` U ) )   &    |- ( ph -> T e. RR+ )   &    |- ( ph -> A. z e. ( X \ { U } ) ( ( z =/= U /\ ( abs ` ( z - U ) ) < T ) -> ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) < ( ( RR _D F ) ` U ) ) )   &    |- S = ( ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) / 2 )   =>    |- -. ph
Theorem	dvferm1 22935*	One-sided version of dvferm 22938. A point U 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.)
|- ( ph -> F : X --> RR )   &    |- ( ph -> X C_ RR )   &    |- ( ph -> U e. ( A (,) B ) )   &    |- ( ph -> ( A (,) B ) C_ X )   &    |- ( ph -> U e. dom ( RR _D F ) )   &    |- ( ph -> A. y e. ( U (,) B ) ( F ` y ) <_ ( F ` U ) )   =>    |- ( ph -> ( ( RR _D F ) ` U ) <_ 0 )
Theorem	dvferm2lem 22936*	Lemma for dvferm 22938. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : X --> RR )   &    |- ( ph -> X C_ RR )   &    |- ( ph -> U e. ( A (,) B ) )   &    |- ( ph -> ( A (,) B ) C_ X )   &    |- ( ph -> U e. dom ( RR _D F ) )   &    |- ( ph -> A. y e. ( A (,) U ) ( F ` y ) <_ ( F ` U ) )   &    |- ( ph -> ( ( RR _D F ) ` U ) < 0 )   &    |- ( ph -> T e. RR+ )   &    |- ( ph -> A. z e. ( X \ { U } ) ( ( z =/= U /\ ( abs ` ( z - U ) ) < T ) -> ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) < -u ( ( RR _D F ) ` U ) ) )   &    |- S = ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) / 2 )   =>    |- -. ph
Theorem	dvferm2 22937*	One-sided version of dvferm 22938. A point U 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.)
|- ( ph -> F : X --> RR )   &    |- ( ph -> X C_ RR )   &    |- ( ph -> U e. ( A (,) B ) )   &    |- ( ph -> ( A (,) B ) C_ X )   &    |- ( ph -> U e. dom ( RR _D F ) )   &    |- ( ph -> A. y e. ( A (,) U ) ( F ` y ) <_ ( F ` U ) )   =>    |- ( ph -> 0 <_ ( ( RR _D F ) ` U ) )
Theorem	dvferm 22938*	Fermat's theorem on stationary points. A point U which is a local maximum has derivative equal to zero. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ph -> F : X --> RR )   &    |- ( ph -> X C_ RR )   &    |- ( ph -> U e. ( A (,) B ) )   &    |- ( ph -> ( A (,) B ) C_ X )   &    |- ( ph -> U e. dom ( RR _D F ) )   &    |- ( ph -> A. y e. ( A (,) B ) ( F ` y ) <_ ( F ` U ) )   =>    |- ( ph -> ( ( RR _D F ) ` U ) = 0 )
Theorem	rollelem 22939*	Lemma for rolle 22940. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` U ) )   &    |- ( ph -> U e. ( A [,] B ) )   &    |- ( ph -> -. U e. { A , B } )   =>    |- ( ph -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )
Theorem	rolle 22940*	Rolle's theorem. If F is a real continuous function on [ A , B ] which is differentiable on ( A , B ), and F ( A ) = F ( B ), then there is some x e. ( A , B ) such that ( RR _D F ) ` x = 0. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> ( F ` A ) = ( F ` B ) )   =>    |- ( ph -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )
Theorem	cmvth 22941*	Cauchy's Mean Value Theorem. If F , G are real continuous functions on [ A , B ] differentiable on ( A , B ), then there is some x e. ( A , B ) such that F' ( x ) / G' ( x ) = ( F ( A ) - F ( B ) ) / ( G ( A ) - G ( B ) ). (We express the condition without division, so that we need no nonzero constraints.) (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> G e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> dom ( RR _D G ) = ( A (,) B ) )   =>    |- ( ph -> E. x e. ( A (,) B ) ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) )
Theorem	mvth 22942*	The Mean Value Theorem. If F is a real continuous function on [ A , B ] which is differentiable on ( A , B ), then there is some x e. ( A , B ) such that ( RR _D F ) ` x is equal to the average slope over [ A , B ]. This is Metamath 100 proof #75. (Contributed by Mario Carneiro, 1-Sep-2014.) (Proof shortened by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   =>    |- ( ph -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = ( ( ( F ` B ) - ( F ` A ) ) / ( B - A ) ) )
Theorem	dvlip 22943*	A function with derivative bounded by M is Lipschitz continuous with Lipschitz constant equal to M. (Contributed by Mario Carneiro, 3-Mar-2015.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> M e. RR )   &    |- ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) <_ M )   =>    |- ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) )
Theorem	dvlipcn 22944*	A complex function with derivative bounded by M on an open ball is Lipschitz continuous with Lipschitz constant equal to M. (Contributed by Mario Carneiro, 18-Mar-2015.)
|- ( ph -> X C_ CC )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> A e. CC )   &    |- ( ph -> R e. RR* )   &    |- B = ( A ( ball ` ( abs o. - ) ) R )   &    |- ( ph -> B C_ dom ( CC _D F ) )   &    |- ( ph -> M e. RR )   &    |- ( ( ph /\ x e. B ) -> ( abs ` ( ( CC _D F ) ` x ) ) <_ M )   =>    |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
Theorem	dvlip2 22945*	Combine the results of dvlip 22943 and dvlipcn 22944 into one. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- J = ( ( abs o. - ) |` ( S X. S ) )   &    |- ( ph -> X C_ S )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> A e. S )   &    |- ( ph -> R e. RR* )   &    |- B = ( A ( ball ` J ) R )   &    |- ( ph -> B C_ dom ( S _D F ) )   &    |- ( ph -> M e. RR )   &    |- ( ( ph /\ x e. B ) -> ( abs ` ( ( S _D F ) ` x ) ) <_ M )   =>    |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
Theorem	c1liplem1 22946*	Lemma for c1lip1 22947. (Contributed by Stefan O'Rear, 15-Nov-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> F e. ( CC ^pm RR ) )   &    |- ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )   &    |- K = sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < )   =>    |- ( ph -> ( K e. RR /\ A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) ) ) )
Theorem	c1lip1 22947*	C1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( CC ^pm RR ) )   &    |- ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )   =>    |- ( ph -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )
Theorem	c1lip2 22948*	C1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( C^n ` RR ) ` 1 ) )   &    |- ( ph -> ran F C_ RR )   &    |- ( ph -> ( A [,] B ) C_ dom F )   =>    |- ( ph -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )
Theorem	c1lip3 22949*	C1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( F |` RR ) e. ( ( C^n ` RR ) ` 1 ) )   &    |- ( ph -> ( F " RR ) C_ RR )   &    |- ( ph -> ( A [,] B ) C_ dom F )   =>    |- ( ph -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )
Theorem	dveq0 22950	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.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )   &    |- ( ph -> ( RR _D F ) = ( ( A (,) B ) X. { 0 } ) )   =>    |- ( ph -> F = ( ( A [,] B ) X. { ( F ` A ) } ) )
Theorem	dv11cn 22951	Two functions defined on a ball whose derivatives are the same and which are equal at any given point C in the ball must be equal everywhere. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- X = ( A ( ball ` ( abs o. - ) ) R )   &    |- ( ph -> A e. CC )   &    |- ( ph -> R e. RR* )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> dom ( CC _D F ) = X )   &    |- ( ph -> ( CC _D F ) = ( CC _D G ) )   &    |- ( ph -> C e. X )   &    |- ( ph -> ( F ` C ) = ( G ` C ) )   =>    |- ( ph -> F = G )
Theorem	dvgt0lem1 22952	Lemma for dvgt0 22954 and dvlt0 22955. (Contributed by Mario Carneiro, 19-Feb-2015.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> ( RR _D F ) : ( A (,) B ) --> S )   =>    |- ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) e. S )
Theorem	dvgt0lem2 22953*	Lemma for dvgt0 22954 and dvlt0 22955. (Contributed by Mario Carneiro, 19-Feb-2015.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> ( RR _D F ) : ( A (,) B ) --> S )   &    |- O Or RR   &    |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` x ) O ( F ` y ) )   =>    |- ( ph -> F Isom < , O ( ( A [,] B ) , ran F ) )
Theorem	dvgt0 22954	A function on a closed interval with positive derivative is increasing. (Contributed by Mario Carneiro, 19-Feb-2015.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> ( RR _D F ) : ( A (,) B ) --> RR+ )   =>    |- ( ph -> F Isom < , < ( ( A [,] B ) , ran F ) )
Theorem	dvlt0 22955	A function on a closed interval with negative derivative is decreasing. (Contributed by Mario Carneiro, 19-Feb-2015.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> ( RR _D F ) : ( A (,) B ) --> ( -oo (,) 0 ) )   =>    |- ( ph -> F Isom < , `' < ( ( A [,] B ) , ran F ) )
Theorem	dvge0 22956	A function on a closed interval with nonnegative derivative is weakly increasing. (Contributed by Mario Carneiro, 30-Apr-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> ( RR _D F ) : ( A (,) B ) --> ( 0 [,) +oo ) )   &    |- ( ph -> X e. ( A [,] B ) )   &    |- ( ph -> Y e. ( A [,] B ) )   &    |- ( ph -> X <_ Y )   =>    |- ( ph -> ( F ` X ) <_ ( F ` Y ) )
Theorem	dvle 22957*	If A ( x ) , C ( x ) are differentiable functions and A ` <_ C ` , then for x <_ y, A ( y ) - A ( x ) <_ C ( y ) - C ( x ). (Contributed by Mario Carneiro, 16-May-2016.)
|- ( ph -> M e. RR )   &    |- ( ph -> N e. RR )   &    |- ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) )   &    |- ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )   &    |- ( ph -> ( x e. ( M [,] N ) |-> C ) e. ( ( M [,] N ) -cn-> RR ) )   &    |- ( ph -> ( RR _D ( x e. ( M (,) N ) |-> C ) ) = ( x e. ( M (,) N ) |-> D ) )   &    |- ( ( ph /\ x e. ( M (,) N ) ) -> B <_ D )   &    |- ( ph -> X e. ( M [,] N ) )   &    |- ( ph -> Y e. ( M [,] N ) )   &    |- ( ph -> X <_ Y )   &    |- ( x = X -> A = P )   &    |- ( x = X -> C = Q )   &    |- ( x = Y -> A = R )   &    |- ( x = Y -> C = S )   =>    |- ( ph -> ( R - P ) <_ ( S - Q ) )
Theorem	dvivthlem1 22958*	Lemma for dvivth 22960. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> M e. ( A (,) B ) )   &    |- ( ph -> N e. ( A (,) B ) )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> M < N )   &    |- ( ph -> C e. ( ( ( RR _D F ) ` N ) [,] ( ( RR _D F ) ` M ) ) )   &    |- G = ( y e. ( A (,) B ) |-> ( ( F ` y ) - ( C x. y ) ) )   =>    |- ( ph -> E. x e. ( M [,] N ) ( ( RR _D F ) ` x ) = C )
Theorem	dvivthlem2 22959*	Lemma for dvivth 22960. (Contributed by Mario Carneiro, 20-Feb-2015.)
|- ( ph -> M e. ( A (,) B ) )   &    |- ( ph -> N e. ( A (,) B ) )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> M < N )   &    |- ( ph -> C e. ( ( ( RR _D F ) ` N ) [,] ( ( RR _D F ) ` M ) ) )   &    |- G = ( y e. ( A (,) B ) |-> ( ( F ` y ) - ( C x. y ) ) )   =>    |- ( ph -> C e. ran ( RR _D F ) )
Theorem	dvivth 22960	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 22407 does not directly apply). (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> M e. ( A (,) B ) )   &    |- ( ph -> N e. ( A (,) B ) )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   =>    |- ( ph -> ( ( ( RR _D F ) ` M ) [,] ( ( RR _D F ) ` N ) ) C_ ran ( RR _D F ) )
Theorem	dvne0 22961	A function on a closed interval with nonzero derivative is either monotone increasing or monotone decreasing. (Contributed by Mario Carneiro, 19-Feb-2015.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> -. 0 e. ran ( RR _D F ) )   =>    |- ( ph -> ( F Isom < , < ( ( A [,] B ) , ran F ) \/ F Isom < , `' < ( ( A [,] B ) , ran F ) ) )
Theorem	dvne0f1 22962	A function on a closed interval with nonzero derivative is one-to-one. (Contributed by Mario Carneiro, 19-Feb-2015.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> -. 0 e. ran ( RR _D F ) )   =>    |- ( ph -> F : ( A [,] B ) -1-1-> RR )
Theorem	lhop1lem 22963*	Lemma for lhop1 22964. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   &    |- ( ph -> F : ( A (,) B ) --> RR )   &    |- ( ph -> G : ( A (,) B ) --> RR )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> dom ( RR _D G ) = ( A (,) B ) )   &    |- ( ph -> 0 e. ( F lim CC A ) )   &    |- ( ph -> 0 e. ( G lim CC A ) )   &    |- ( ph -> -. 0 e. ran G )   &    |- ( ph -> -. 0 e. ran ( RR _D G ) )   &    |- ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) lim CC A ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> D <_ B )   &    |- ( ph -> X e. ( A (,) D ) )   &    |- ( ph -> A. t e. ( A (,) D ) ( abs ` ( ( ( ( RR _D F ) ` t ) / ( ( RR _D G ) ` t ) ) - C ) ) < E )   &    |- R = ( A + ( r / 2 ) )   =>    |- ( ph -> ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) < ( 2 x. E ) )
Theorem	lhop1 22964*	L'Hôpital's Rule for limits from the right. If F and G are differentiable real functions on ( A , B ), and F and G both approach 0 at A, and G ( x ) and G' ( x ) are not zero on ( A , B ), and the limit of F' ( x ) / G' ( x ) at A is C, then the limit F ( x ) / G ( x ) at A also exists and equals C. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   &    |- ( ph -> F : ( A (,) B ) --> RR )   &    |- ( ph -> G : ( A (,) B ) --> RR )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> dom ( RR _D G ) = ( A (,) B ) )   &    |- ( ph -> 0 e. ( F lim CC A ) )   &    |- ( ph -> 0 e. ( G lim CC A ) )   &    |- ( ph -> -. 0 e. ran G )   &    |- ( ph -> -. 0 e. ran ( RR _D G ) )   &    |- ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) lim CC A ) )   =>    |- ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) lim CC A ) )
Theorem	lhop2 22965*	L'Hôpital's Rule for limits from the left. If F and G are differentiable real functions on ( A , B ), and F and G both approach 0 at B, and G ( x ) and G' ( x ) are not zero on ( A , B ), and the limit of F' ( x ) / G' ( x ) at B is C, then the limit F ( x ) / G ( x ) at B also exists and equals C. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F : ( A (,) B ) --> RR )   &    |- ( ph -> G : ( A (,) B ) --> RR )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> dom ( RR _D G ) = ( A (,) B ) )   &    |- ( ph -> 0 e. ( F lim CC B ) )   &    |- ( ph -> 0 e. ( G lim CC B ) )   &    |- ( ph -> -. 0 e. ran G )   &    |- ( ph -> -. 0 e. ran ( RR _D G ) )   &    |- ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) lim CC B ) )   =>    |- ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) lim CC B ) )
Theorem	lhop 22966*	L'Hôpital's Rule. If I is an open set of the reals, F and G are real functions on A containing all of I except possibly B, which are differentiable everywhere on I \ { B }, F and G both approach 0, and the limit of F' ( x ) / G' ( x ) at B is C, then the limit F ( x ) / G ( x ) at B also exists and equals C. This is Metamath 100 proof #64. (Contributed by Mario Carneiro, 30-Dec-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> G : A --> RR )   &    |- ( ph -> I e. ( topGen ` ran (,) ) )   &    |- ( ph -> B e. I )   &    |- D = ( I \ { B } )   &    |- ( ph -> D C_ dom ( RR _D F ) )   &    |- ( ph -> D C_ dom ( RR _D G ) )   &    |- ( ph -> 0 e. ( F lim CC B ) )   &    |- ( ph -> 0 e. ( G lim CC B ) )   &    |- ( ph -> -. 0 e. ( G " D ) )   &    |- ( ph -> -. 0 e. ( ( RR _D G ) " D ) )   &    |- ( ph -> C e. ( ( z e. D |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) lim CC B ) )   =>    |- ( ph -> C e. ( ( z e. D |-> ( ( F ` z ) / ( G ` z ) ) ) lim CC B ) )
Theorem	dvcnvrelem1 22967	Lemma for dvcnvre 22969. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F e. ( X -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = X )   &    |- ( ph -> -. 0 e. ran ( RR _D F ) )   &    |- ( ph -> F : X -1-1-onto-> Y )   &    |- ( ph -> C e. X )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> ( ( C - R ) [,] ( C + R ) ) C_ X )   =>    |- ( ph -> ( F ` C ) e. ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
Theorem	dvcnvrelem2 22968	Lemma for dvcnvre 22969. (Contributed by Mario Carneiro, 19-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
|- ( ph -> F e. ( X -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = X )   &    |- ( ph -> -. 0 e. ran ( RR _D F ) )   &    |- ( ph -> F : X -1-1-onto-> Y )   &    |- ( ph -> C e. X )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> ( ( C - R ) [,] ( C + R ) ) C_ X )   &    |- T = ( topGen ` ran (,) )   &    |- J = ( TopOpen ` ℂfld )   &    |- M = ( J ↾t X )   &    |- N = ( J ↾t Y )   =>    |- ( ph -> ( ( F ` C ) e. ( ( int ` T ) ` Y ) /\ `' F e. ( ( N CnP M ) ` ( F ` C ) ) ) )
Theorem	dvcnvre 22969*	The derivative rule for inverse functions. If F is a continuous and differentiable bijective function from X to Y which never has derivative 0, then `' F is also differentiable, and its derivative is the reciprocal of the derivative of F. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F e. ( X -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = X )   &    |- ( ph -> -. 0 e. ran ( RR _D F ) )   &    |- ( ph -> F : X -1-1-onto-> Y )   =>    |- ( ph -> ( RR _D `' F ) = ( x e. Y |-> ( 1 / ( ( RR _D F ) ` ( `' F ` x ) ) ) ) )
Theorem	dvcvx 22970	A real function with strictly increasing derivative is strictly convex. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   &    |- ( ph -> ( RR _D F ) Isom < , < ( ( A (,) B ) , W ) )   &    |- ( ph -> T e. ( 0 (,) 1 ) )   &    |- C = ( ( T x. A ) + ( ( 1 - T ) x. B ) )   =>    |- ( ph -> ( F ` C ) < ( ( T x. ( F ` A ) ) + ( ( 1 - T ) x. ( F ` B ) ) ) )
Theorem	dvfsumle 22971*	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.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) )   &    |- ( ( ph /\ x e. ( M (,) N ) ) -> B e. V )   &    |- ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )   &    |- ( x = M -> A = C )   &    |- ( x = N -> A = D )   &    |- ( ( ph /\ k e. ( M..^ N ) ) -> X e. RR )   &    |- ( ( ph /\ ( k e. ( M..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> X <_ B )   =>    |- ( ph -> sum_ k e. ( M..^ N ) X <_ ( D - C ) )
Theorem	dvfsumge 22972*	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.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) )   &    |- ( ( ph /\ x e. ( M (,) N ) ) -> B e. V )   &    |- ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )   &    |- ( x = M -> A = C )   &    |- ( x = N -> A = D )   &    |- ( ( ph /\ k e. ( M..^ N ) ) -> X e. RR )   &    |- ( ( ph /\ ( k e. ( M..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> B <_ X )   =>    |- ( ph -> ( D - C ) <_ sum_ k e. ( M..^ N ) X )
Theorem	dvfsumabs 22973*	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.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> CC ) )   &    |- ( ( ph /\ x e. ( M (,) N ) ) -> B e. V )   &    |- ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )   &    |- ( x = M -> A = C )   &    |- ( x = N -> A = D )   &    |- ( ( ph /\ k e. ( M..^ N ) ) -> X e. CC )   &    |- ( ( ph /\ k e. ( M..^ N ) ) -> Y e. RR )   &    |- ( ( ph /\ ( k e. ( M..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> ( abs ` ( X - B ) ) <_ Y )   =>    |- ( ph -> ( abs ` ( sum_ k e. ( M..^ N ) X - ( D - C ) ) ) <_ sum_ k e. ( M..^ N ) Y )
Theorem	dvmptrecl 22974*	Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016.)
|- ( ph -> S C_ RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   =>    |- ( ( ph /\ x e. S ) -> B e. RR )
Theorem	dvfsumrlimf 22975*	Lemma for dvfsumrlim 22981. (Contributed by Mario Carneiro, 18-May-2016.)
|- S = ( T (,) +oo )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> M <_ ( D + 1 ) )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ( ph /\ x e. Z ) -> B e. RR )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   &    |- ( x = k -> B = C )   &    |- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )   =>    |- ( ph -> G : S --> RR )
Theorem	dvfsumlem1 22976*	Lemma for dvfsumrlim 22981. (Contributed by Mario Carneiro, 17-May-2016.)
|- S = ( T (,) +oo )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> M <_ ( D + 1 ) )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ( ph /\ x e. Z ) -> B e. RR )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   &    |- ( x = k -> B = C )   &    |- ( ph -> U e. RR* )   &    |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )   &    |- H = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   &    |- ( ph -> D <_ X )   &    |- ( ph -> X <_ Y )   &    |- ( ph -> Y <_ U )   &    |- ( ph -> Y <_ ( ( |_ ` X ) + 1 ) )   =>    |- ( ph -> ( H ` Y ) = ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )
Theorem	dvfsumlem2 22977*	Lemma for dvfsumrlim 22981. (Contributed by Mario Carneiro, 17-May-2016.)
|- S = ( T (,) +oo )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> M <_ ( D + 1 ) )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ( ph /\ x e. Z ) -> B e. RR )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   &    |- ( x = k -> B = C )   &    |- ( ph -> U e. RR* )   &    |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )   &    |- H = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   &    |- ( ph -> D <_ X )   &    |- ( ph -> X <_ Y )   &    |- ( ph -> Y <_ U )   &    |- ( ph -> Y <_ ( ( |_ ` X ) + 1 ) )   =>    |- ( ph -> ( ( H ` Y ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )
Theorem	dvfsumlem3 22978*	Lemma for dvfsumrlim 22981. (Contributed by Mario Carneiro, 17-May-2016.)
|- S = ( T (,) +oo )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> M <_ ( D + 1 ) )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ( ph /\ x e. Z ) -> B e. RR )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   &    |- ( x = k -> B = C )   &    |- ( ph -> U e. RR* )   &    |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )   &    |- H = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   &    |- ( ph -> D <_ X )   &    |- ( ph -> X <_ Y )   &    |- ( ph -> Y <_ U )   =>    |- ( ph -> ( ( H ` Y ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )
Theorem	dvfsumlem4 22979*	Lemma for dvfsumrlim 22981. (Contributed by Mario Carneiro, 18-May-2016.)
|- S = ( T (,) +oo )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> M <_ ( D + 1 ) )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ( ph /\ x e. Z ) -> B e. RR )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   &    |- ( x = k -> B = C )   &    |- ( ph -> U e. RR* )   &    |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )   &    |- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )   &    |- ( ( ph /\ ( x e. S /\ D <_ x /\ x <_ U ) ) -> 0 <_ B )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   &    |- ( ph -> D <_ X )   &    |- ( ph -> X <_ Y )   &    |- ( ph -> Y <_ U )   =>    |- ( ph -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) <_ [_ X / x ]_ B )
Theorem	dvfsumrlimge0 22980*	Lemma for dvfsumrlim 22981. Satisfy the assumption of dvfsumlem4 22979. (Contributed by Mario Carneiro, 18-May-2016.)
|- S = ( T (,) +oo )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> M <_ ( D + 1 ) )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ( ph /\ x e. Z ) -> B e. RR )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   &    |- ( x = k -> B = C )   &    |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k ) ) -> C <_ B )   &    |- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )   &    |- ( ph -> ( x e. S |-> B ) ~~> r 0 )   =>    |- ( ( ph /\ ( x e. S /\ D <_ x ) ) -> 0 <_ B )
Theorem	dvfsumrlim 22981*	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 x e. S |-> B is a decreasing function with antiderivative A converging to zero, then the difference between sum_ k e. ( M ... ( |_ ` x ) ) B ( k ) and A ( x ) = S. u e. ( M [,] x ) B ( u ) _d u converges to a constant limit value, with the remainder term bounded by B ( x ). (Contributed by Mario Carneiro, 18-May-2016.)
|- S = ( T (,) +oo )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> M <_ ( D + 1 ) )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ( ph /\ x e. Z ) -> B e. RR )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   &    |- ( x = k -> B = C )   &    |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k ) ) -> C <_ B )   &    |- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )   &    |- ( ph -> ( x e. S |-> B ) ~~> r 0 )   =>    |- ( ph -> G e. dom ~~> r )
Theorem	dvfsumrlim2 22982*	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 x e. S |-> B is a decreasing function with antiderivative A converging to zero, then the difference between sum_ k e. ( M ... ( |_ ` x ) ) B ( k ) and S. u e. ( M [,] x ) B ( u ) _d u = A ( x ) converges to a constant limit value, with the remainder term bounded by B ( x ). (Contributed by Mario Carneiro, 18-May-2016.)
|- S = ( T (,) +oo )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> M <_ ( D + 1 ) )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ( ph /\ x e. Z ) -> B e. RR )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   &    |- ( x = k -> B = C )   &    |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k ) ) -> C <_ B )   &    |- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )   &    |- ( ph -> ( x e. S |-> B ) ~~> r 0 )   &    |- ( ph -> X e. S )   &    |- ( ph -> D <_ X )   =>    |- ( ( ph /\ G ~~> r L ) -> ( abs ` ( ( G ` X ) - L ) ) <_ [_ X / x ]_ B )
Theorem	dvfsumrlim3 22983*	Conjoin the statements of dvfsumrlim 22981 and dvfsumrlim2 22982. (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.)
|- S = ( T (,) +oo )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> M <_ ( D + 1 ) )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ( ph /\ x e. Z ) -> B e. RR )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   &    |- ( x = k -> B = C )   &    |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k ) ) -> C <_ B )   &    |- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )   &    |- ( ph -> ( x e. S |-> B ) ~~> r 0 )   &    |- ( x = X -> B = E )   =>    |- ( ph -> ( G : S --> RR /\ G e. dom ~~> r /\ ( ( G ~~> r L /\ X e. S /\ D <_ X ) -> ( abs ` ( ( G ` X ) - L ) ) <_ E ) ) )
Theorem	dvfsum2 22984*	The reverse of dvfsumrlim 22981, 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.)
|- S = ( T (,) +oo )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> U e. RR* )   &    |- ( ph -> M <_ ( D + 1 ) )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ x e. S ) -> B e. V )   &    |- ( ( ph /\ x e. Z ) -> B e. RR )   &    |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )   &    |- ( x = k -> B = C )   &    |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> B <_ C )   &    |- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )   &    |- ( ( ph /\ ( x e. S /\ D <_ x ) ) -> 0 <_ B )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   &    |- ( ph -> D <_ X )   &    |- ( ph -> X <_ Y )   &    |- ( ph -> Y <_ U )   &    |- ( x = Y -> B = E )   =>    |- ( ph -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) <_ E )
Theorem	ftc1lem1 22985*	Lemma for ftc1a 22987 and ftc1 22992. (Contributed by Mario Carneiro, 31-Aug-2014.)
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> ( A (,) B ) C_ D )   &    |- ( ph -> D C_ RR )   &    |- ( ph -> F e. L^1 )   &    |- ( ph -> F : D --> CC )   &    |- ( ph -> X e. ( A [,] B ) )   &    |- ( ph -> Y e. ( A [,] B ) )   =>    |- ( ( ph /\ X <_ Y ) -> ( ( G ` Y ) - ( G ` X ) ) = S. ( X (,) Y ) ( F ` t ) _d t )
Theorem	ftc1lem2 22986*	Lemma for ftc1 22992. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> ( A (,) B ) C_ D )   &    |- ( ph -> D C_ RR )   &    |- ( ph -> F e. L^1 )   &    |- ( ph -> F : D --> CC )   =>    |- ( ph -> G : ( A [,] B ) --> CC )
Theorem	ftc1a 22987*	The Fundamental Theorem of Calculus, part one. The function G formed by varying the right endpoint of an integral of F is continuous if F is integrable. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> ( A (,) B ) C_ D )   &    |- ( ph -> D C_ RR )   &    |- ( ph -> F e. L^1 )   &    |- ( ph -> F : D --> CC )   =>    |- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )
Theorem	ftc1lem3 22988*	Lemma for ftc1 22992. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 8-Sep-2015.)
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> ( A (,) B ) C_ D )   &    |- ( ph -> D C_ RR )   &    |- ( ph -> F e. L^1 )   &    |- ( ph -> C e. ( A (,) B ) )   &    |- ( ph -> F e. ( ( K CnP L ) ` C ) )   &    |- J = ( L ↾t RR )   &    |- K = ( L ↾t D )   &    |- L = ( TopOpen ` ℂfld )   =>    |- ( ph -> F : D --> CC )
Theorem	ftc1lem4 22989*	Lemma for ftc1 22992. (Contributed by Mario Carneiro, 31-Aug-2014.)
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> ( A (,) B ) C_ D )   &    |- ( ph -> D C_ RR )   &    |- ( ph -> F e. L^1 )   &    |- ( ph -> C e. ( A (,) B ) )   &    |- ( ph -> F e. ( ( K CnP L ) ` C ) )   &    |- J = ( L ↾t RR )   &    |- K = ( L ↾t D )   &    |- L = ( TopOpen ` ℂfld )   &    |- H = ( z e. ( ( A [,] B ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ y e. D ) -> ( ( abs ` ( y - C ) ) < R -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < E ) )   &    |- ( ph -> X e. ( A [,] B ) )   &    |- ( ph -> ( abs ` ( X - C ) ) < R )   &    |- ( ph -> Y e. ( A [,] B ) )   &    |- ( ph -> ( abs ` ( Y - C ) ) < R )   =>    |- ( ( ph /\ X < Y ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` X ) ) / ( Y - X ) ) - ( F ` C ) ) ) < E )
Theorem	ftc1lem5 22990*	Lemma for ftc1 22992. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> ( A (,) B ) C_ D )   &    |- ( ph -> D C_ RR )   &    |- ( ph -> F e. L^1 )   &    |- ( ph -> C e. ( A (,) B ) )   &    |- ( ph -> F e. ( ( K CnP L ) ` C ) )   &    |- J = ( L ↾t RR )   &    |- K = ( L ↾t D )   &    |- L = ( TopOpen ` ℂfld )   &    |- H = ( z e. ( ( A [,] B ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ y e. D ) -> ( ( abs ` ( y - C ) ) < R -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < E ) )   &    |- ( ph -> X e. ( A [,] B ) )   &    |- ( ph -> ( abs ` ( X - C ) ) < R )   =>    |- ( ( ph /\ X =/= C ) -> ( abs ` ( ( H ` X ) - ( F ` C ) ) ) < E )
Theorem	ftc1lem6 22991*	Lemma for ftc1 22992. (Contributed by Mario Carneiro, 14-Aug-2014.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> ( A (,) B ) C_ D )   &    |- ( ph -> D C_ RR )   &    |- ( ph -> F e. L^1 )   &    |- ( ph -> C e. ( A (,) B ) )   &    |- ( ph -> F e. ( ( K CnP L ) ` C ) )   &    |- J = ( L ↾t RR )   &    |- K = ( L ↾t D )   &    |- L = ( TopOpen ` ℂfld )   &    |- H = ( z e. ( ( A [,] B ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) )   =>    |- ( ph -> ( F ` C ) e. ( H lim CC C ) )
Theorem	ftc1 22992*	The Fundamental Theorem of Calculus, part one. The function formed by varying the right endpoint of an integral is differentiable at C with derivative F ( C ) if the original function is continuous at C. This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> ( A (,) B ) C_ D )   &    |- ( ph -> D C_ RR )   &    |- ( ph -> F e. L^1 )   &    |- ( ph -> C e. ( A (,) B ) )   &    |- ( ph -> F e. ( ( K CnP L ) ` C ) )   &    |- J = ( L ↾t RR )   &    |- K = ( L ↾t D )   &    |- L = ( TopOpen ` ℂfld )   =>    |- ( ph -> C ( RR _D G ) ( F ` C ) )
Theorem	ftc1cn 22993*	Strengthen the assumptions of ftc1 22992 to when the function F is continuous on the entire interval ( A , B ); in this case we can calculate _D G exactly. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> F e. L^1 )   =>    |- ( ph -> ( RR _D G ) = F )
Theorem	ftc2 22994*	The Fundamental Theorem of Calculus, part two. If F is a function continuous on [ A , B ] and continuously differentiable on ( A , B ), then the integral of the derivative of F is equal to F ( B ) - F ( A ). This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 2-Sep-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> ( RR _D F ) e. L^1 )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )   =>    |- ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )
Theorem	ftc2ditglem 22995*	Lemma for ftc2ditg 22996. (Contributed by Mario Carneiro, 3-Sep-2014.)
|- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> A e. ( X [,] Y ) )   &    |- ( ph -> B e. ( X [,] Y ) )   &    |- ( ph -> ( RR _D F ) e. ( ( X (,) Y ) -cn-> CC ) )   &    |- ( ph -> ( RR _D F ) e. L^1 )   &    |- ( ph -> F e. ( ( X [,] Y ) -cn-> CC ) )   =>    |- ( ( ph /\ A <_ B ) -> S__ [ A -> B ] ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )
Theorem	ftc2ditg 22996*	Directed integral analog of ftc2 22994. (Contributed by Mario Carneiro, 3-Sep-2014.)
|- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> A e. ( X [,] Y ) )   &    |- ( ph -> B e. ( X [,] Y ) )   &    |- ( ph -> ( RR _D F ) e. ( ( X (,) Y ) -cn-> CC ) )   &    |- ( ph -> ( RR _D F ) e. L^1 )   &    |- ( ph -> F e. ( ( X [,] Y ) -cn-> CC ) )   =>    |- ( ph -> S__ [ A -> B ] ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )
Theorem	itgparts 22997*	Integration by parts. If B ( x ) is the derivative of A ( x ) and D ( x ) is the derivative of C ( x ), and E = ( A x. B ) ( X ) and F = ( A x. B ) ( Y ), then under suitable integrability and differentiability assumptions, the integral of A x. D from X to Y is equal to F - E minus the integral of B x. C. (Contributed by Mario Carneiro, 3-Sep-2014.)
|- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> X <_ Y )   &    |- ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> CC ) )   &    |- ( ph -> ( x e. ( X [,] Y ) |-> C ) e. ( ( X [,] Y ) -cn-> CC ) )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( X (,) Y ) -cn-> CC ) )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> D ) e. ( ( X (,) Y ) -cn-> CC ) )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> ( A x. D ) ) e. L^1 )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> ( B x. C ) ) e. L^1 )   &    |- ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )   &    |- ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> C ) ) = ( x e. ( X (,) Y ) |-> D ) )   &    |- ( ( ph /\ x = X ) -> ( A x. C ) = E )   &    |- ( ( ph /\ x = Y ) -> ( A x. C ) = F )   =>    |- ( ph -> S. ( X (,) Y ) ( A x. D ) _d x = ( ( F - E ) - S. ( X (,) Y ) ( B x. C ) _d x ) )
Theorem	itgsubstlem 22998*	Lemma for itgsubst 22999. (Contributed by Mario Carneiro, 12-Sep-2014.)
|- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> X <_ Y )   &    |- ( ph -> Z e. RR* )   &    |- ( ph -> W e. RR* )   &    |- ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )   &    |- ( ph -> ( u e. ( Z (,) W ) |-> C ) e. ( ( Z (,) W ) -cn-> CC ) )   &    |- ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )   &    |- ( u = A -> C = E )   &    |- ( x = X -> A = K )   &    |- ( x = Y -> A = L )   &    |- ( ph -> M e. ( Z (,) W ) )   &    |- ( ph -> N e. ( Z (,) W ) )   &    |- ( ( ph /\ x e. ( X [,] Y ) ) -> A e. ( M (,) N ) )   =>    |- ( ph -> S__ [ K -> L ] C _d u = S__ [ X -> Y ] ( E x. B ) _d x )
Theorem	itgsubst 22999*	Integration by u-substitution. If A ( x ) is a continuous, differentiable function from [ X , Y ] to ( Z , W ), whose derivative is continuous and integrable, and C ( u ) is a continuous function on ( Z , W ), then the integral of C ( u ) from K = A ( X ) to L = A ( Y ) is equal to the integral of C ( A ( x ) ) _D A ( x ) from X to Y. In this part of the proof we discharge the assumptions in itgsubstlem 22998, which use the fact that ( Z , W ) is open to shrink the interval a little to ( M , N ) where Z < M < N < W- this is possible because A ( x ) 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.)
|- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> X <_ Y )   &    |- ( ph -> Z e. RR* )   &    |- ( ph -> W e. RR* )   &    |- ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )   &    |- ( ph -> ( u e. ( Z (,) W ) |-> C ) e. ( ( Z (,) W ) -cn-> CC ) )   &    |- ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )   &    |- ( u = A -> C = E )   &    |- ( x = X -> A = K )   &    |- ( x = Y -> A = L )   =>    |- ( ph -> S__ [ K -> L ] C _d u = S__ [ X -> Y ] ( E x. B ) _d x )
PART 14  BASIC REAL AND COMPLEX FUNCTIONS
14.1  Polynomials
14.1.1  Polynomial degrees
Syntax	cmdg 23000	Multivariate polynomial degree.
class mDeg