P. 227 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22601-22700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	perfdvf 22601	The derivative is a function, whenever it is defined relative to a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- K = ( TopOpen ` ℂfld )   =>    |- ( ( K ↾t S ) e. Perf -> ( S _D F ) : dom ( S _D F ) --> CC )
Theorem	recnprss 22602	Both RR and CC are subsets of CC. (Contributed by Mario Carneiro, 10-Feb-2015.)
|- ( S e. { RR , CC } -> S C_ CC )
Theorem	recnperf 22603	Both RR and CC are perfect subsets of CC. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- K = ( TopOpen ` ℂfld )   =>    |- ( S e. { RR , CC } -> ( K ↾t S ) e. Perf )
Theorem	dvfg 22604	Explicitly write out the functionality condition on derivative for S = RR and CC. (Contributed by Mario Carneiro, 9-Feb-2015.)
|- ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
Theorem	dvf 22605	The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( RR _D F ) : dom ( RR _D F ) --> CC
Theorem	dvfcn 22606	The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.)
|- ( CC _D F ) : dom ( CC _D F ) --> CC
Theorem	dvreslem 22607*	Lemma for dvres 22609. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- K = ( TopOpen ` ℂfld )   &    |- T = ( K ↾t S )   &    |- G = ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   &    |- ( ph -> B C_ S )   &    |- ( ph -> y e. CC )   =>    |- ( ph -> ( x ( S _D ( F |` B ) ) y <-> ( x ( S _D F ) y /\ x e. ( ( int ` T ) ` B ) ) ) )
Theorem	dvres2lem 22608*	Lemma for dvres2 22610. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- K = ( TopOpen ` ℂfld )   &    |- T = ( K ↾t S )   &    |- G = ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   &    |- ( ph -> B C_ S )   &    |- ( ph -> y e. CC )   &    |- ( ph -> x ( S _D F ) y )   &    |- ( ph -> x e. B )   =>    |- ( ph -> x ( B _D ( F |` B ) ) y )
Theorem	dvres 22609	Restriction of a derivative. Note that our definition of derivative df-dv 22565 would still make sense if we demanded that x be an element of the domain instead of an interior point of the domain, but then it is possible for a non-differentiable function to have two different derivatives at a single point x when restricted to different subsets containing x; a classic example is the absolute value function restricted to [ 0 , +oo ) and ( -oo , 0 ]. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- K = ( TopOpen ` ℂfld )   &    |- T = ( K ↾t S )   =>    |- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( S _D ( F |` B ) ) = ( ( S _D F ) |` ( ( int ` T ) ` B ) ) )
Theorem	dvres2 22610	Restriction of the base set of a derivative. The primary application of this theorem says that if a function is complex differentiable then it is also real differentiable. Unlike dvres 22609, there is no simple reverse relation relating real differentiable functions to complex differentiability, and indeed there are functions like Re ( x ) which are everywhere real-differentiable but nowhere complex-differentiable.) (Contributed by Mario Carneiro, 9-Feb-2015.)
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( S _D F ) |` B ) C_ ( B _D ( F |` B ) ) )
Theorem	dvres3 22611	Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015.)
|- ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> ( S _D ( F |` S ) ) = ( ( CC _D F ) |` S ) )
Theorem	dvres3a 22612	Restriction of a complex differentiable function to the reals. This version of dvres3 22611 assumes that F is differentiable on its domain, but does not require F to be differentiable on the whole real line. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A e. J /\ dom ( CC _D F ) = A ) ) -> ( S _D ( F |` S ) ) = ( ( CC _D F ) |` S ) )
Theorem	dvidlem 22613*	Lemma for dvid 22615 and dvconst 22614. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( ph -> F : CC --> CC )   &    |- ( ( ph /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( CC _D F ) = ( CC X. { B } ) )
Theorem	dvconst 22614	Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( A e. CC -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
Theorem	dvid 22615	Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )
Theorem	dvcnp 22616*	The difference quotient is continuous at B when the original function is differentiable at B. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- J = ( K ↾t A )   &    |- K = ( TopOpen ` ℂfld )   &    |- G = ( z e. A |-> if ( z = B , ( ( S _D F ) ` B ) , ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) )   =>    |- ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> G e. ( ( J CnP K ) ` B ) )
Theorem	dvcnp2 22617	A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- J = ( K ↾t A )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> F e. ( ( J CnP K ) ` B ) )
Theorem	dvcn 22618	A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
|- ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> F e. ( A -cn-> CC ) )
Theorem	dvnfval 22619*	Value of the iterated derivative. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- G = ( x e. _V |-> ( S _D x ) )   =>    |- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) = seq 0 ( ( G o. 1st ) , ( NN0 X. { F } ) ) )
Theorem	dvnff 22620	The iterated derivative is a function. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) : NN0 --> ( CC ^pm dom F ) )
Theorem	dvn0 22621	Zero times iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
Theorem	dvnp1 22622	Successor iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` ( N + 1 ) ) = ( S _D ( ( S Dn F ) ` N ) ) )
Theorem	dvn1 22623	One times iterated derivative. (Contributed by Mario Carneiro, 1-Jan-2017.)
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 1 ) = ( S _D F ) )
Theorem	dvnf 22624	The N-times derivative is a function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC )
Theorem	dvnbss 22625	The set of N-times differentiable points is a subset of the domain of the function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> dom ( ( S Dn F ) ` N ) C_ dom F )
Theorem	dvnadd 22626	The N-th derivative of the M-th derivative of F is the same as the M + N-th derivative of F. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` N ) = ( ( S Dn F ) ` ( M + N ) ) )
Theorem	dvn2bss 22627	An N-times differentiable point is an M-times differentiable point, if M <_ N. (Contributed by Mario Carneiro, 30-Dec-2016.)
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` M ) )
Theorem	dvnres 22628	Multiple derivative version of dvres3a 22612. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) /\ N e. NN0 ) /\ dom ( ( CC Dn F ) ` N ) = dom F ) -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) )
Theorem	cpnfval 22629*	Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( S C_ CC -> ( C^n ` S ) = ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) )
Theorem	fncpn 22630	The C^n object is a function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( S C_ CC -> ( C^n ` S ) Fn NN0 )
Theorem	elcpn 22631	Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S C_ CC /\ N e. NN0 ) -> ( F e. ( ( C^n ` S ) ` N ) <-> ( F e. ( CC ^pm S ) /\ ( ( S Dn F ) ` N ) e. ( dom F -cn-> CC ) ) ) )
Theorem	cpnord 22632	C^n conditions are ordered by strength. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( ( C^n ` S ) ` N ) C_ ( ( C^n ` S ) ` M ) )
Theorem	cpncn 22633	A C^n function is continuous. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> F e. ( dom F -cn-> CC ) )
Theorem	cpnres 22634	The restriction of a C^n function is C^n. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( F |` S ) e. ( ( C^n ` S ) ` N ) )
Theorem	dvaddbr 22635	The sum rule for derivatives at a point. For the (simpler but more limited) function version, see dvadd 22637. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : Y --> CC )   &    |- ( ph -> Y C_ S )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> K e. V )   &    |- ( ph -> L e. V )   &    |- ( ph -> C ( S _D F ) K )   &    |- ( ph -> C ( S _D G ) L )   &    |- J = ( TopOpen ` ℂfld )   =>    |- ( ph -> C ( S _D ( F oF + G ) ) ( K + L ) )
Theorem	dvmulbr 22636	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 22638. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : Y --> CC )   &    |- ( ph -> Y C_ S )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> K e. V )   &    |- ( ph -> L e. V )   &    |- ( ph -> C ( S _D F ) K )   &    |- ( ph -> C ( S _D G ) L )   &    |- J = ( TopOpen ` ℂfld )   =>    |- ( ph -> C ( S _D ( F oF x. G ) ) ( ( K x. ( G ` C ) ) + ( L x. ( F ` C ) ) ) )
Theorem	dvadd 22637	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddbr 22635. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : Y --> CC )   &    |- ( ph -> Y C_ S )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> C e. dom ( S _D F ) )   &    |- ( ph -> C e. dom ( S _D G ) )   =>    |- ( ph -> ( ( S _D ( F oF + G ) ) ` C ) = ( ( ( S _D F ) ` C ) + ( ( S _D G ) ` C ) ) )
Theorem	dvmul 22638	The product rule for derivatives at a point. For the (more general) relation version, see dvmulbr 22636. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : Y --> CC )   &    |- ( ph -> Y C_ S )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> C e. dom ( S _D F ) )   &    |- ( ph -> C e. dom ( S _D G ) )   =>    |- ( ph -> ( ( S _D ( F oF x. G ) ) ` C ) = ( ( ( ( S _D F ) ` C ) x. ( G ` C ) ) + ( ( ( S _D G ) ` C ) x. ( F ` C ) ) ) )
Theorem	dvaddf 22639	The sum rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> dom ( S _D F ) = X )   &    |- ( ph -> dom ( S _D G ) = X )   =>    |- ( ph -> ( S _D ( F oF + G ) ) = ( ( S _D F ) oF + ( S _D G ) ) )
Theorem	dvmulf 22640	The product rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> dom ( S _D F ) = X )   &    |- ( ph -> dom ( S _D G ) = X )   =>    |- ( ph -> ( S _D ( F oF x. G ) ) = ( ( ( S _D F ) oF x. G ) oF + ( ( S _D G ) oF x. F ) ) )
Theorem	dvcmul 22641	The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> A e. CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> C e. dom ( S _D F ) )   =>    |- ( ph -> ( ( S _D ( ( S X. { A } ) oF x. F ) ) ` C ) = ( A x. ( ( S _D F ) ` C ) ) )
Theorem	dvcmulf 22642	The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> A e. CC )   &    |- ( ph -> dom ( S _D F ) = X )   =>    |- ( ph -> ( S _D ( ( S X. { A } ) oF x. F ) ) = ( ( S X. { A } ) oF x. ( S _D F ) ) )
Theorem	dvcobr 22643	The chain rule for derivatives at a point. For the (simpler but more limited) function version, see dvco 22644. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : Y --> X )   &    |- ( ph -> Y C_ T )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> T C_ CC )   &    |- ( ph -> K e. V )   &    |- ( ph -> L e. V )   &    |- ( ph -> ( G ` C ) ( S _D F ) K )   &    |- ( ph -> C ( T _D G ) L )   &    |- J = ( TopOpen ` ℂfld )   =>    |- ( ph -> C ( T _D ( F o. G ) ) ( K x. L ) )
Theorem	dvco 22644	The chain rule for derivatives at a point. For the (more general) relation version, see dvcobr 22643. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : Y --> X )   &    |- ( ph -> Y C_ T )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> T e. { RR , CC } )   &    |- ( ph -> ( G ` C ) e. dom ( S _D F ) )   &    |- ( ph -> C e. dom ( T _D G ) )   =>    |- ( ph -> ( ( T _D ( F o. G ) ) ` C ) = ( ( ( S _D F ) ` ( G ` C ) ) x. ( ( T _D G ) ` C ) ) )
Theorem	dvcof 22645	The chain rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 10-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> T e. { RR , CC } )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : Y --> X )   &    |- ( ph -> dom ( S _D F ) = X )   &    |- ( ph -> dom ( T _D G ) = Y )   =>    |- ( ph -> ( T _D ( F o. G ) ) = ( ( ( S _D F ) o. G ) oF x. ( T _D G ) ) )
Theorem	dvcjbr 22646	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 22647. (This doesn't follow from dvcobr 22643 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 22647	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 22646. (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 22648	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 22649	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 22650*	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 22651*	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 22652*	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 22653*	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 22654*	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 22655*	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 22656*	Closure lemma for dvmptcmul 22661 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 22657*	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 22658*	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 22659*	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 22660*	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 22661*	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 22662*	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 22663*	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 22664*	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 22665*	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 22666*	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 22667*	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 22668*	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 22669*	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 22670*	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 22671	Lemma for dvcnvre 22714. (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 22672*	A weak version of dvcnvre 22714, 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 22673*	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 22674	Derivative of the exponential function at 0. The key step in the proof is eftlub 14055, 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 22675	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 22676	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 22677	Derivative of the sine function. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( CC _D sin ) = cos
Theorem	dvcos 22678	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 22679*	Lemma for dvferm 22683. (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 22680*	One-sided version of dvferm 22683. 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 22681*	Lemma for dvferm 22683. (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 22682*	One-sided version of dvferm 22683. 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 22683*	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 22684*	Lemma for rolle 22685. (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 22685*	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 22686*	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 22687*	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 22688*	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 22689*	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 22690*	Combine the results of dvlip 22688 and dvlipcn 22689 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 22691*	Lemma for c1lip1 22692. (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 22692*	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 22693*	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 22694*	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 22695	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 22696	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 22697	Lemma for dvgt0 22699 and dvlt0 22700. (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 22698*	Lemma for dvgt0 22699 and dvlt0 22700. (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 22699	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 22700	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 ) )