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
Definition	df-dv 22901*	Define the derivative operator on functions on the reals. This acts on functions to produce a function that is defined where the original function is differentiable, with value the derivative of the function at these points. The set s here is the ambient topological space under which we are evaluating the continuity of the difference quotient. Although the definition is valid for any subset of CC and is well-behaved when s contains no isolated points, we will restrict our attention to the cases s = RR or s = CC for the majority of the development, these corresponding respectively to real and complex differentiation. (Contributed by Mario Carneiro, 7-Aug-2014.)
|- _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )
Definition	df-dvn 22902*	Define the n-th derivative operator on functions on the complex numbers. This just iterates the derivative operation according to the last argument. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- Dn = ( s e. ~P CC , f e. ( CC ^pm s ) |-> seq 0 ( ( ( x e. _V |-> ( s _D x ) ) o. 1st ) , ( NN0 X. { f } ) ) )
Definition	df-cpn 22903*	Define the set of n-times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014.)
|- C^n = ( s e. ~P CC |-> ( x e. NN0 |-> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC ) } ) )
Theorem	reldv 22904	The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- Rel ( S _D F )
Theorem	limcvallem 22905*	Lemma for ellimc 22907. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- J = ( K ↾t ( A u. { B } ) )   &    |- K = ( TopOpen ` ℂfld )   &    |- G = ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) )   =>    |- ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( G e. ( ( J CnP K ) ` B ) -> C e. CC ) )
Theorem	limcfval 22906*	Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- J = ( K ↾t ( A u. { B } ) )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( ( F lim CC B ) = { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } /\ ( F lim CC B ) C_ CC ) )
Theorem	ellimc 22907*	Value of the limit predicate. C is the limit of the function F at B if the function G, formed by adding B to the domain of F and setting it to C, is continuous at B. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- J = ( K ↾t ( A u. { B } ) )   &    |- K = ( TopOpen ` ℂfld )   &    |- G = ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( C e. ( F lim CC B ) <-> G e. ( ( J CnP K ) ` B ) ) )
Theorem	limcrcl 22908	Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( C e. ( F lim CC B ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
Theorem	limccl 22909	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( F lim CC B ) C_ CC
Theorem	limcdif 22910	It suffices to consider functions which are not defined at B to define the limit of a function. In particular, the value of the original function F at B does not affect the limit of F. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   =>    |- ( ph -> ( F lim CC B ) = ( ( F |` ( A \ { B } ) ) lim CC B ) )
Theorem	ellimc2 22911*	Write the definition of a limit directly in terms of open sets of the topology on the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> ( C e. ( F lim CC B ) <-> ( C e. CC /\ A. u e. K ( C e. u -> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) ) ) )
Theorem	limcnlp 22912	If B is not a limit point of the domain of the function F, then every point is a limit of F at B. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- K = ( TopOpen ` ℂfld )   &    |- ( ph -> -. B e. ( ( limPt ` K ) ` A ) )   =>    |- ( ph -> ( F lim CC B ) = CC )
Theorem	ellimc3 22913*	Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( C e. ( F lim CC B ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )
Theorem	limcflflem 22914	Lemma for limcflf 22915. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. ( ( limPt ` K ) ` A ) )   &    |- K = ( TopOpen ` ℂfld )   &    |- C = ( A \ { B } )   &    |- L = ( ( ( nei ` K ) ` { B } ) ↾t C )   =>    |- ( ph -> L e. ( Fil ` C ) )
Theorem	limcflf 22915	The limit operator can be expressed as a filter limit, from the filter of neighborhoods of B restricted to A \ { B }, to the topology of the complex numbers. (If B is not a limit point of A, then it is still formally a filter limit, but the neighborhood filter is not a proper filter in this case.) (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. ( ( limPt ` K ) ` A ) )   &    |- K = ( TopOpen ` ℂfld )   &    |- C = ( A \ { B } )   &    |- L = ( ( ( nei ` K ) ` { B } ) ↾t C )   =>    |- ( ph -> ( F lim CC B ) = ( ( K fLimf L ) ` ( F |` C ) ) )
Theorem	limcmo 22916*	If B is a limit point of the domain of the function F, then there is at most one limit value of F at B. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. ( ( limPt ` K ) ` A ) )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> E* x x e. ( F lim CC B ) )
Theorem	limcmpt 22917*	Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- ( ( ph /\ z e. A ) -> D e. CC )   &    |- J = ( K ↾t ( A u. { B } ) )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> ( C e. ( ( z e. A |-> D ) lim CC B ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , C , D ) ) e. ( ( J CnP K ) ` B ) ) )
Theorem	limcmpt2 22918*	Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> A C_ CC )   &    |- ( ph -> B e. A )   &    |- ( ( ph /\ ( z e. A /\ z =/= B ) ) -> D e. CC )   &    |- J = ( K ↾t A )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> ( C e. ( ( z e. ( A \ { B } ) |-> D ) lim CC B ) <-> ( z e. A |-> if ( z = B , C , D ) ) e. ( ( J CnP K ) ` B ) ) )
Theorem	limcresi 22919	Any limit of F is also a limit of the restriction of F. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( F lim CC B ) C_ ( ( F |` C ) lim CC B )
Theorem	limcres 22920	If B is an interior point of C u. { B } relative to the domain A, then a limit point of F |` C extends to a limit of F. (Contributed by Mario Carneiro, 27-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> C C_ A )   &    |- ( ph -> A C_ CC )   &    |- K = ( TopOpen ` ℂfld )   &    |- J = ( K ↾t ( A u. { B } ) )   &    |- ( ph -> B e. ( ( int ` J ) ` ( C u. { B } ) ) )   =>    |- ( ph -> ( ( F |` C ) lim CC B ) = ( F lim CC B ) )
Theorem	cnplimc 22921	A function is continuous at B iff its limit at B equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- K = ( TopOpen ` ℂfld )   &    |- J = ( K ↾t A )   =>    |- ( ( A C_ CC /\ B e. A ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F : A --> CC /\ ( F ` B ) e. ( F lim CC B ) ) ) )
Theorem	cnlimc 22922*	F is a continuous function iff the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( A C_ CC -> ( F e. ( A -cn-> CC ) <-> ( F : A --> CC /\ A. x e. A ( F ` x ) e. ( F lim CC x ) ) ) )
Theorem	cnlimci 22923	If F is a continuous function, then the limit of the function at any point equals its value. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> F e. ( A -cn-> D ) )   &    |- ( ph -> B e. A )   =>    |- ( ph -> ( F ` B ) e. ( F lim CC B ) )
Theorem	cnmptlimc 22924*	If F is a continuous function, then the limit of the function at any point equals its value. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> ( x e. A |-> X ) e. ( A -cn-> D ) )   &    |- ( ph -> B e. A )   &    |- ( x = B -> X = Y )   =>    |- ( ph -> Y e. ( ( x e. A |-> X ) lim CC B ) )
Theorem	limccnp 22925	If the limit of F at B is C and G is continuous at C, then the limit of G o. F at B is G ( C ). (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> F : A --> D )   &    |- ( ph -> D C_ CC )   &    |- K = ( TopOpen ` ℂfld )   &    |- J = ( K ↾t D )   &    |- ( ph -> C e. ( F lim CC B ) )   &    |- ( ph -> G e. ( ( J CnP K ) ` C ) )   =>    |- ( ph -> ( G ` C ) e. ( ( G o. F ) lim CC B ) )
Theorem	limccnp2 22926*	The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ( ph /\ x e. A ) -> R e. X )   &    |- ( ( ph /\ x e. A ) -> S e. Y )   &    |- ( ph -> X C_ CC )   &    |- ( ph -> Y C_ CC )   &    |- K = ( TopOpen ` ℂfld )   &    |- J = ( ( K tX K ) ↾t ( X X. Y ) )   &    |- ( ph -> C e. ( ( x e. A |-> R ) lim CC B ) )   &    |- ( ph -> D e. ( ( x e. A |-> S ) lim CC B ) )   &    |- ( ph -> H e. ( ( J CnP K ) ` <. C , D >. ) )   =>    |- ( ph -> ( C H D ) e. ( ( x e. A |-> ( R H S ) ) lim CC B ) )
Theorem	limcco 22927*	Composition of two limits. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ( ph /\ ( x e. A /\ R =/= C ) ) -> R e. B )   &    |- ( ( ph /\ y e. B ) -> S e. CC )   &    |- ( ph -> C e. ( ( x e. A |-> R ) lim CC X ) )   &    |- ( ph -> D e. ( ( y e. B |-> S ) lim CC C ) )   &    |- ( y = R -> S = T )   &    |- ( ( ph /\ ( x e. A /\ R = C ) ) -> T = D )   =>    |- ( ph -> D e. ( ( x e. A |-> T ) lim CC X ) )
Theorem	limciun 22928*	A point is a limit of F on the finite union U_ x e. A B ( x ) iff it is the limit of the restriction of F to each B ( x ). (Contributed by Mario Carneiro, 30-Dec-2016.)
|- ( ph -> A e. Fin )   &    |- ( ph -> A. x e. A B C_ CC )   &    |- ( ph -> F : U_ x e. A B --> CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( F lim CC C ) = ( CC i^i |^|_ x e. A ( ( F |` B ) lim CC C ) ) )
Theorem	limcun 22929	A point is a limit of F on A u. B iff it is the limit of the restriction of F to A and to B. (Contributed by Mario Carneiro, 30-Dec-2016.)
|- ( ph -> A C_ CC )   &    |- ( ph -> B C_ CC )   &    |- ( ph -> F : ( A u. B ) --> CC )   =>    |- ( ph -> ( F lim CC C ) = ( ( ( F |` A ) lim CC C ) i^i ( ( F |` B ) lim CC C ) ) )
Theorem	dvlem 22930	Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( ph -> F : D --> CC )   &    |- ( ph -> D C_ CC )   &    |- ( ph -> B e. D )   =>    |- ( ( ph /\ A e. ( D \ { B } ) ) -> ( ( ( F ` A ) - ( F ` B ) ) / ( A - B ) ) e. CC )
Theorem	dvfval 22931*	Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 25-Dec-2016.)
|- T = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( ( S _D F ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) lim CC x ) ) /\ ( S _D F ) C_ ( ( ( int ` T ) ` A ) X. CC ) ) )
Theorem	eldv 22932*	The differentiable predicate. A function F is differentiable at B with derivative C iff F is defined in a neighborhood of B and the difference quotient has limit C at B. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 25-Dec-2016.)
|- T = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   &    |- G = ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   =>    |- ( ph -> ( B ( S _D F ) C <-> ( B e. ( ( int ` T ) ` A ) /\ C e. ( G lim CC B ) ) ) )
Theorem	dvcl 22933	The derivative function takes values in the complex numbers. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   =>    |- ( ( ph /\ B ( S _D F ) C ) -> C e. CC )
Theorem	dvbssntr 22934	The set of differentiable points is a subset of the interior of the domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   &    |- J = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> dom ( S _D F ) C_ ( ( int ` J ) ` A ) )
Theorem	dvbss 22935	The set of differentiable points is a subset of the domain of the function. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   =>    |- ( ph -> dom ( S _D F ) C_ A )
Theorem	dvbsss 22936	The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.)
|- dom ( S _D F ) C_ S
Theorem	perfdvf 22937	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 22938	Both RR and CC are subsets of CC. (Contributed by Mario Carneiro, 10-Feb-2015.)
|- ( S e. { RR , CC } -> S C_ CC )
Theorem	recnperf 22939	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 22940	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 22941	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 22942	The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.)
|- ( CC _D F ) : dom ( CC _D F ) --> CC
Theorem	dvreslem 22943*	Lemma for dvres 22945. (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 22944*	Lemma for dvres2 22946. (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 22945	Restriction of a derivative. Note that our definition of derivative df-dv 22901 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 22946	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 22945, 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 22947	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 22948	Restriction of a complex differentiable function to the reals. This version of dvres3 22947 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 22949*	Lemma for dvid 22951 and dvconst 22950. (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 22950	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 22951	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 22952*	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 22953	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 22954	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 22955*	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 22956	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 22957	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 22958	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 22959	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 22960	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 22961	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 22962	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 22963	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 22964	Multiple derivative version of dvres3a 22948. (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 22965*	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 22966	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 22967	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 22968	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 22969	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 22970	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 22971	The sum rule for derivatives at a point. For the (simpler but more limited) function version, see dvadd 22973. (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 22972	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 22974. (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 22973	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddbr 22971. (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 22974	The product rule for derivatives at a point. For the (more general) relation version, see dvmulbr 22972. (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 22975	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 22976	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 22977	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 22978	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 22979	The chain rule for derivatives at a point. For the (simpler but more limited) function version, see dvco 22980. (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 22980	The chain rule for derivatives at a point. For the (more general) relation version, see dvcobr 22979. (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 22981	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 22982	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 22983. (This doesn't follow from dvcobr 22979 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 22983	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 22982. (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 22984	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 22985	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 22986*	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 22987*	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 22988*	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 22989*	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 22990*	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 22991*	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 22992*	Closure lemma for dvmptcmul 22997 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 22993*	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 22994*	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 22995*	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 22996*	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 22997*	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 22998*	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 22999*	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 23000*	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 ) ) )