P. 129 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	limcmpted 12801*	Express the limit operator for a function defined by a mapping, via epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.)
|- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- ( ( ph /\ z e. A ) -> D e. CC )   =>    |- ( ph -> ( C e. ( ( z e. A |-> D ) 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 ` ( D - C ) ) < x ) ) ) )
Theorem	limcimolemlt 12802*	Lemma for limcimo 12803. (Contributed by Jim Kingdon, 3-Jul-2023.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B e. C )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. ( K ↾t S ) )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> { q e. C | q # B } C_ A )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> X e. ( F lim CC B ) )   &    |- ( ph -> Y e. ( F lim CC B ) )   &    |- ( ph -> A. z e. A ( ( z # B /\ ( abs ` ( z - B ) ) < D ) -> ( abs ` ( ( F ` z ) - X ) ) < ( ( abs ` ( X - Y ) ) / 2 ) ) )   &    |- ( ph -> G e. RR+ )   &    |- ( ph -> A. w e. A ( ( w # B /\ ( abs ` ( w - B ) ) < G ) -> ( abs ` ( ( F ` w ) - Y ) ) < ( ( abs ` ( X - Y ) ) / 2 ) ) )   =>    |- ( ph -> ( abs ` ( X - Y ) ) < ( abs ` ( X - Y ) ) )
Theorem	limcimo 12803*	Conditions which ensure there is at most one limit value of F at B. (Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon, 8-Jul-2023.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B e. C )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. ( K ↾t S ) )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> { q e. C | q # B } C_ A )   &    |- K = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> E* x x e. ( F lim CC B ) )
Theorem	limcresi 12804	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	cnplimcim 12805	If a function is continuous at B, its limit at B equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 14-Jun-2023.)
|- K = ( MetOpen ` ( abs o. - ) )   &    |- 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	cnplimclemle 12806	Lemma for cnplimccntop 12808. Satisfying the epsilon condition for continuity. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
|- K = ( MetOpen ` ( abs o. - ) )   &    |- J = ( K ↾t A )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> B e. A )   &    |- ( ph -> ( F ` B ) e. ( F lim CC B ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> Z e. A )   &    |- ( ( ph /\ Z # B /\ ( abs ` ( Z - B ) ) < D ) -> ( abs ` ( ( F ` Z ) - ( F ` B ) ) ) < ( E / 2 ) )   &    |- ( ph -> ( abs ` ( Z - B ) ) < D )   =>    |- ( ph -> ( abs ` ( ( F ` Z ) - ( F ` B ) ) ) < E )
Theorem	cnplimclemr 12807	Lemma for cnplimccntop 12808. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
|- K = ( MetOpen ` ( abs o. - ) )   &    |- J = ( K ↾t A )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> B e. A )   &    |- ( ph -> ( F ` B ) e. ( F lim CC B ) )   =>    |- ( ph -> F e. ( ( J CnP K ) ` B ) )
Theorem	cnplimccntop 12808	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 = ( MetOpen ` ( abs o. - ) )   &    |- 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	cnlimcim 12809*	If F is a continuous function, the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 16-Jun-2023.)
|- ( A C_ CC -> ( F e. ( A -cn-> CC ) -> ( F : A --> CC /\ A. x e. A ( F ` x ) e. ( F lim CC x ) ) ) )
Theorem	cnlimc 12810*	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 12811	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 12812*	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	limccnpcntop 12813	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.) (Revised by Jim Kingdon, 18-Jun-2023.)
|- ( ph -> F : A --> D )   &    |- ( ph -> D C_ CC )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- 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	limccnp2lem 12814*	Lemma for limccnp2cntop 12815. This is most of the result, expressed in epsilon-delta form, with a large number of hypotheses so that lengthy expressions do not need to be repeated. (Contributed by Jim Kingdon, 9-Nov-2023.)
|- ( ( ph /\ x e. A ) -> R e. X )   &    |- ( ( ph /\ x e. A ) -> S e. Y )   &    |- ( ph -> X C_ CC )   &    |- ( ph -> Y C_ CC )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- 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 >. ) )   &    |- F/ x ph   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> L e. RR+ )   &    |- ( ph -> A. r e. X A. s e. Y ( ( ( C ( ( abs o. - ) |` ( X X. X ) ) r ) < L /\ ( D ( ( abs o. - ) |` ( Y X. Y ) ) s ) < L ) -> ( ( C H D ) ( abs o. - ) ( r H s ) ) < E ) )   &    |- ( ph -> F e. RR+ )   &    |- ( ph -> A. x e. A ( ( x # B /\ ( abs ` ( x - B ) ) < F ) -> ( abs ` ( R - C ) ) < L ) )   &    |- ( ph -> G e. RR+ )   &    |- ( ph -> A. x e. A ( ( x # B /\ ( abs ` ( x - B ) ) < G ) -> ( abs ` ( S - D ) ) < L ) )   =>    |- ( ph -> E. d e. RR+ A. x e. A ( ( x # B /\ ( abs ` ( x - B ) ) < d ) -> ( abs ` ( ( R H S ) - ( C H D ) ) ) < E ) )
Theorem	limccnp2cntop 12815*	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.) (Revised by Jim Kingdon, 14-Nov-2023.)
|- ( ( ph /\ x e. A ) -> R e. X )   &    |- ( ( ph /\ x e. A ) -> S e. Y )   &    |- ( ph -> X C_ CC )   &    |- ( ph -> Y C_ CC )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- 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	limccoap 12816*	Composition of two limits. This theorem is only usable in the case where x # X implies R(x) # C so it is less general than might appear at first. (Contributed by Mario Carneiro, 29-Dec-2016.) (Revised by Jim Kingdon, 18-Dec-2023.)
|- ( ( ph /\ x e. { w e. A | w # X } ) -> R e. { w e. B | w # C } )   &    |- ( ( ph /\ y e. { w e. B | w # C } ) -> S e. CC )   &    |- ( ph -> C e. ( ( x e. { w e. A | w # X } |-> R ) lim CC X ) )   &    |- ( ph -> D e. ( ( y e. { w e. B | w # C } |-> S ) lim CC C ) )   &    |- ( y = R -> S = T )   =>    |- ( ph -> D e. ( ( x e. { w e. A | w # X } |-> T ) lim CC X ) )
Theorem	reldvg 12817	The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.)
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> Rel ( S _D F ) )
Theorem	dvlemap 12818*	Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|- ( ph -> F : D --> CC )   &    |- ( ph -> D C_ CC )   &    |- ( ph -> B e. D )   =>    |- ( ( ph /\ A e. { w e. D | w # B } ) -> ( ( ( F ` A ) - ( F ` B ) ) / ( A - B ) ) e. CC )
Theorem	dvfvalap 12819*	Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|- T = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   =>    |- ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( ( S _D F ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. { w e. A | w # x } |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) lim CC x ) ) /\ ( S _D F ) C_ ( ( ( int ` T ) ` A ) X. CC ) ) )
Theorem	eldvap 12820*	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 Jim Kingdon, 27-Jun-2023.)
|- T = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- G = ( z e. { w e. A | w # 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 12821	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	dvbssntrcntop 12822	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 Jim Kingdon, 27-Jun-2023.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   &    |- J = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> dom ( S _D F ) C_ ( ( int ` J ) ` A ) )
Theorem	dvbss 12823	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	dvbsssg 12824	The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Jim Kingdon, 28-Jun-2023.)
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> dom ( S _D F ) C_ S )
Theorem	recnprss 12825	Both RR and CC are subsets of CC. (Contributed by Mario Carneiro, 10-Feb-2015.)
|- ( S e. { RR , CC } -> S C_ CC )
Theorem	dvfgg 12826	Explicitly write out the functionality condition on derivative for S = RR and CC. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jun-2023.)
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( S _D F ) : dom ( S _D F ) --> CC )
Theorem	dvfpm 12827	The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.)
|- ( F e. ( CC ^pm RR ) -> ( RR _D F ) : dom ( RR _D F ) --> CC )
Theorem	dvfcnpm 12828	The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.)
|- ( F e. ( CC ^pm CC ) -> ( CC _D F ) : dom ( CC _D F ) --> CC )
Theorem	dvidlemap 12829*	Lemma for dvid 12831 and dvconst 12830. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|- ( 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 12830	Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|- ( A e. CC -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
Theorem	dvid 12831	Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|- ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )
Theorem	dvcnp2cntop 12832	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 = ( MetOpen ` ( abs o. - ) )   =>    |- ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> F e. ( ( J CnP K ) ` B ) )
Theorem	dvcn 12833	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	dvaddxxbr 12834	The sum rule for derivatives at a point. That is, if the derivative of F at C is K and the derivative of G at C is L, then the derivative of the pointwise sum of those two functions at C is K + L. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> C ( S _D F ) K )   &    |- ( ph -> C ( S _D G ) L )   &    |- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> C ( S _D ( F oF + G ) ) ( K + L ) )
Theorem	dvmulxxbr 12835	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 12837. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> C ( S _D F ) K )   &    |- ( ph -> C ( S _D G ) L )   &    |- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> C ( S _D ( F oF x. G ) ) ( ( K x. ( G ` C ) ) + ( L x. ( F ` C ) ) ) )
Theorem	dvaddxx 12836	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 12834. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : X --> CC )   &    |- ( 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	dvmulxx 12837	The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 12835. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : X --> CC )   &    |- ( 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	dviaddf 12838	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 -> X C_ S )   &    |- ( 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	dvimulf 12839	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 -> X C_ S )   &    |- ( 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	dvcoapbr 12840*	The chain rule for derivatives at a point. The u # C -> ( G ` u ) # ( G ` C ) hypothesis constrains what functions work for G. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 21-Dec-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : Y --> X )   &    |- ( ph -> Y C_ T )   &    |- ( ph -> A. u e. Y ( u # C -> ( G ` u ) # ( G ` C ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> T C_ CC )   &    |- ( ph -> ( G ` C ) ( S _D F ) K )   &    |- ( ph -> C ( T _D G ) L )   &    |- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> C ( T _D ( F o. G ) ) ( K x. L ) )
Theorem	dvcjbr 12841	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 12842. (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 12842	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 12841. (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 12843	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	dvexp 12844*	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 12845*	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	dvrecap 12846*	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. { w e. CC | w # 0 } |-> ( A / x ) ) ) = ( x e. { w e. CC | w # 0 } |-> -u ( A / ( x ^ 2 ) ) ) )
Theorem	dvmptidcn 12847	Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.)
|- ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 )
Theorem	dvmptccn 12848*	Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> 0 ) )
Theorem	dvmptclx 12849*	Closure lemma for dvmptmulx 12851 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 C_ S )   =>    |- ( ( ph /\ x e. X ) -> B e. CC )
Theorem	dvmptaddx 12850*	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 C_ S )   &    |- ( ( 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	dvmptmulx 12851*	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 C_ S )   &    |- ( ( 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	dvmptcmulcn 12852*	Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
|- ( ( ph /\ x e. CC ) -> A e. CC )   &    |- ( ( ph /\ x e. CC ) -> B e. V )   &    |- ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> B ) )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( CC _D ( x e. CC |-> ( C x. A ) ) ) = ( x e. CC |-> ( C x. B ) ) )
Theorem	dvmptnegcn 12853*	Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
|- ( ( ph /\ x e. CC ) -> A e. CC )   &    |- ( ( ph /\ x e. CC ) -> B e. V )   &    |- ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> B ) )   =>    |- ( ph -> ( CC _D ( x e. CC |-> -u A ) ) = ( x e. CC |-> -u B ) )
Theorem	dvmptsubcn 12854*	Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
|- ( ( ph /\ x e. CC ) -> A e. CC )   &    |- ( ( ph /\ x e. CC ) -> B e. V )   &    |- ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> B ) )   &    |- ( ( ph /\ x e. CC ) -> C e. CC )   &    |- ( ( ph /\ x e. CC ) -> D e. W )   &    |- ( ph -> ( CC _D ( x e. CC |-> C ) ) = ( x e. CC |-> D ) )   =>    |- ( ph -> ( CC _D ( x e. CC |-> ( A - C ) ) ) = ( x e. CC |-> ( B - D ) ) )
Theorem	dveflem 12855	Derivative of the exponential function at 0. The key step in the proof is eftlub 11396, 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 12856	Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
|- ( CC _D exp ) = exp
PART 9  BASIC REAL AND COMPLEX FUNCTIONS
9.1  Basic trigonometry
9.1.1  The exponential, sine, and cosine functions (cont.)
Theorem	efcn 12857	The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
|- exp e. ( CC -cn-> CC )
Theorem	sincn 12858	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- sin e. ( CC -cn-> CC )
Theorem	coscn 12859	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- cos e. ( CC -cn-> CC )
9.1.2  Properties of pi = 3.14159...
Theorem	pilem1 12860	Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro, 9-May-2014.)
|- ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ ( sin ` A ) = 0 ) )
Theorem	cosz12 12861	Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.)
|- E. p e. ( 1 (,) 2 ) ( cos ` p ) = 0
Theorem	sin0pilem1 12862*	Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
|- E. p e. ( 1 (,) 2 ) ( ( cos ` p ) = 0 /\ A. x e. ( p (,) ( 2 x. p ) ) 0 < ( sin ` x ) )
Theorem	sin0pilem2 12863*	Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
|- E. q e. ( 2 (,) 4 ) ( ( sin ` q ) = 0 /\ A. x e. ( 0 (,) q ) 0 < ( sin ` x ) )
Theorem	pilem3 12864	Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )
Theorem	pigt2lt4 12865	pi is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- ( 2 < pi /\ pi < 4 )
Theorem	sinpi 12866	The sine of pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` pi ) = 0
Theorem	pire 12867	pi is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
|- pi e. RR
Theorem	picn 12868	pi is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- pi e. CC
Theorem	pipos 12869	pi is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- 0 < pi
Theorem	pirp 12870	pi is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- pi e. RR+
Theorem	negpicn 12871	-u pi is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u pi e. CC
Theorem	sinhalfpilem 12872	Lemma for sinhalfpi 12877 and coshalfpi 12878. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( ( sin ` ( pi / 2 ) ) = 1 /\ ( cos ` ( pi / 2 ) ) = 0 )
Theorem	halfpire 12873	pi / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
|- ( pi / 2 ) e. RR
Theorem	neghalfpire 12874	-u pi / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR
Theorem	neghalfpirx 12875	-u pi / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR*
Theorem	pidiv2halves 12876	Adding pi / 2 to itself gives pi. See 2halves 8949. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
Theorem	sinhalfpi 12877	The sine of pi / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( pi / 2 ) ) = 1
Theorem	coshalfpi 12878	The cosine of pi / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( pi / 2 ) ) = 0
Theorem	cosneghalfpi 12879	The cosine of -u pi / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
|- ( cos ` -u ( pi / 2 ) ) = 0
Theorem	efhalfpi 12880	The exponential of _i pi / 2 is _i. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( pi / 2 ) ) ) = _i
Theorem	cospi 12881	The cosine of pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` pi ) = -u 1
Theorem	efipi 12882	The exponential of _i x. pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( exp ` ( _i x. pi ) ) = -u 1
Theorem	eulerid 12883	Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- ( ( exp ` ( _i x. pi ) ) + 1 ) = 0
Theorem	sin2pi 12884	The sine of 2 pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( 2 x. pi ) ) = 0
Theorem	cos2pi 12885	The cosine of 2 pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( 2 x. pi ) ) = 1
Theorem	ef2pi 12886	The exponential of 2 pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( 2 x. pi ) ) ) = 1
Theorem	ef2kpi 12887	If K is an integer, then the exponential of 2 K pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( K e. ZZ -> ( exp ` ( ( _i x. ( 2 x. pi ) ) x. K ) ) = 1 )
Theorem	efper 12888	The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( A + ( ( _i x. ( 2 x. pi ) ) x. K ) ) ) = ( exp ` A ) )
Theorem	sinperlem 12889	Lemma for sinper 12890 and cosper 12891. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( A e. CC -> ( F ` A ) = ( ( ( exp ` ( _i x. A ) ) O ( exp ` ( -u _i x. A ) ) ) / D ) )   &    |- ( ( A + ( K x. ( 2 x. pi ) ) ) e. CC -> ( F ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( ( ( exp ` ( _i x. ( A + ( K x. ( 2 x. pi ) ) ) ) ) O ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. pi ) ) ) ) ) ) / D ) )   =>    |- ( ( A e. CC /\ K e. ZZ ) -> ( F ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( F ` A ) )
Theorem	sinper 12890	The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( sin ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( sin ` A ) )
Theorem	cosper 12891	The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( cos ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( cos ` A ) )
Theorem	sin2kpi 12892	If K is an integer, then the sine of 2 K pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( K e. ZZ -> ( sin ` ( K x. ( 2 x. pi ) ) ) = 0 )
Theorem	cos2kpi 12893	If K is an integer, then the cosine of 2 K pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( K e. ZZ -> ( cos ` ( K x. ( 2 x. pi ) ) ) = 1 )
Theorem	sin2pim 12894	Sine of a number subtracted from 2 x. pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( ( 2 x. pi ) - A ) ) = -u ( sin ` A ) )
Theorem	cos2pim 12895	Cosine of a number subtracted from 2 x. pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( ( 2 x. pi ) - A ) ) = ( cos ` A ) )
Theorem	sinmpi 12896	Sine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( A - pi ) ) = -u ( sin ` A ) )
Theorem	cosmpi 12897	Cosine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( A - pi ) ) = -u ( cos ` A ) )
Theorem	sinppi 12898	Sine of a number plus pi. (Contributed by NM, 10-Aug-2008.)
|- ( A e. CC -> ( sin ` ( A + pi ) ) = -u ( sin ` A ) )
Theorem	cosppi 12899	Cosine of a number plus pi. (Contributed by NM, 18-Aug-2008.)
|- ( A e. CC -> ( cos ` ( A + pi ) ) = -u ( cos ` A ) )
Theorem	efimpi 12900	The exponential function at _i times a real number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( exp ` ( _i x. ( A - pi ) ) ) = -u ( exp ` ( _i x. A ) ) )