P. 151 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-dvap 15001*	Define the derivative operator. 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.) (Revised by Jim Kingdon, 25-Jun-2023.)
|- _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( MetOpen ` ( abs o. - ) ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. { w e. dom f | w # x } |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )
Theorem	limcrcl 15002	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 15003	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( F lim CC B ) C_ CC
Theorem	ellimc3apf 15004*	Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 4-Nov-2023.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- F/_ z F   =>    |- ( 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	ellimc3ap 15005*	Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) Use apartness. (Revised by Jim Kingdon, 3-Jun-2023.)
|- ( 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	limcdifap 15006*	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.) (Revised by Jim Kingdon, 3-Jun-2023.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   =>    |- ( ph -> ( F lim CC B ) = ( ( F |` { x e. A | x # B } ) lim CC B ) )
Theorem	limcmpted 15007*	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 15008*	Lemma for limcimo 15009. (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 15009*	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 15010	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 15011	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 15012	Lemma for cnplimccntop 15014. 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 15013	Lemma for cnplimccntop 15014. 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 15014	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 15015*	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 15016*	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 15017	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 15018*	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 15019	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 15020*	Lemma for limccnp2cntop 15021. 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 15021*	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 15022*	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 15023	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 15024*	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 15025*	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 15026*	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 15027	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 15028	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 15029	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 15030	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 15031	Both RR and CC are subsets of CC. (Contributed by Mario Carneiro, 10-Feb-2015.)
|- ( S e. { RR , CC } -> S C_ CC )
Theorem	dvfgg 15032	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 15033	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 15034	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 15035*	Lemma for dvid 15039 and dvconst 15038. (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	dvidrelem 15036*	Lemma for dvidre 15041 and dvconstre 15040. Analogue of dvidlemap 15035 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( ph -> F : RR --> CC )   &    |- ( ( ph /\ ( x e. RR /\ z e. RR /\ z # x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( RR _D F ) = ( RR X. { B } ) )
Theorem	dvidsslem 15037*	Lemma for dvconstss 15042. Analogue of dvidlemap 15035 where F is defined on an open subset of the real or complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( ph -> S e. { RR , CC } )   &    |- J = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> X e. J )   &    |- ( ( ph /\ ( x e. X /\ z e. X /\ z # x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( S _D F ) = ( X X. { B } ) )
Theorem	dvconst 15038	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 15039	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	dvconstre 15040	Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( A e. CC -> ( RR _D ( RR X. { A } ) ) = ( RR X. { 0 } ) )
Theorem	dvidre 15041	Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( RR _D ( _I |` RR ) ) = ( RR X. { 1 } )
Theorem	dvconstss 15042	Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.)
|- ( ph -> S e. { RR , CC } )   &    |- J = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> X e. J )   &    |- ( ph -> A e. CC )   =>    |- ( ph -> ( S _D ( X X. { A } ) ) = ( X X. { 0 } ) )
Theorem	dvcnp2cntop 15043	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 15044	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 15045	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 15046	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 15048. (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 15047	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 15045. (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 15048	The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 15046. (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 15049	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 15050	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 15051*	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 15052	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 15053. (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 15053	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 15052. (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 15054	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 15055*	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 15056*	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 15057*	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 15058	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 15059*	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	dvmptid 15060*	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 15061*	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	dvmptclx 15062*	Closure lemma for dvmptmulx 15064 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 15063*	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 15064*	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 15065*	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 15066*	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 15067*	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	dvmptcjx 15068*	Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.)
|- ( ( 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 -> X C_ RR )   =>    |- ( ph -> ( RR _D ( x e. X |-> ( * ` A ) ) ) = ( x e. X |-> ( * ` B ) ) )
Theorem	dvmptfsum 15069*	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	dveflem 15070	Derivative of the exponential function at 0. The key step in the proof is eftlub 11874, 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 15071	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 11  BASIC REAL AND COMPLEX FUNCTIONS
11.1  Polynomials
11.1.1  Elementary properties of complex polynomials
Syntax	cply 15072	Extend class notation to include the set of complex polynomials.
class Poly
Syntax	cidp 15073	Extend class notation to include the identity polynomial.
class Xp
Definition	df-ply 15074*	Define the set of polynomials on the complex numbers with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- Poly = ( x e. ~P CC |-> { f | E. n e. NN0 E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )
Definition	df-idp 15075	Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- Xp = ( _I |` CC )
Theorem	plyval 15076*	Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- ( S C_ CC -> (Poly ` S ) = { f | E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )
Theorem	plybss 15077	Reverse closure of the parameter S of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( F e. (Poly ` S ) -> S C_ CC )
Theorem	elply 15078*	Definition of a polynomial with coefficients in S. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- ( F e. (Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
Theorem	elply2 15079*	The coefficient function can be assumed to have zeroes outside 0 ... n. (Contributed by Mario Carneiro, 20-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( F e. (Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
Theorem	plyun0 15080	The set of polynomials is unaffected by the addition of zero. (This is built into the definition because all higher powers of a polynomial are effectively zero, so we require that the coefficient field contain zero to simplify some of our closure theorems.) (Contributed by Mario Carneiro, 17-Jul-2014.)
|- (Poly ` ( S u. { 0 } ) ) = (Poly ` S )
Theorem	plyf 15081	A polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( F e. (Poly ` S ) -> F : CC --> CC )
Theorem	plyss 15082	The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- ( ( S C_ T /\ T C_ CC ) -> (Poly ` S ) C_ (Poly ` T ) )
Theorem	plyssc 15083	Every polynomial ring is contained in the ring of polynomials over CC. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- (Poly ` S ) C_ (Poly ` CC )
Theorem	elplyr 15084*	Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) e. (Poly ` S ) )
Theorem	elplyd 15085*	Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- ( ph -> S C_ CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ k e. ( 0 ... N ) ) -> A e. S )   =>    |- ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) e. (Poly ` S ) )
Theorem	ply1termlem 15086*	Lemma for ply1term 15087. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- F = ( z e. CC |-> ( A x. ( z ^ N ) ) )   =>    |- ( ( A e. CC /\ N e. NN0 ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) ) )
Theorem	ply1term 15087*	A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- F = ( z e. CC |-> ( A x. ( z ^ N ) ) )   =>    |- ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> F e. (Poly ` S ) )
Theorem	plypow 15088*	A power is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- ( ( S C_ CC /\ 1 e. S /\ N e. NN0 ) -> ( z e. CC |-> ( z ^ N ) ) e. (Poly ` S ) )
Theorem	plyconst 15089	A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- ( ( S C_ CC /\ A e. S ) -> ( CC X. { A } ) e. (Poly ` S ) )
Theorem	plyid 15090	The identity function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- ( ( S C_ CC /\ 1 e. S ) -> Xp e. (Poly ` S ) )
Theorem	plyaddlem1 15091*	Derive the coefficient function for the sum of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> B : NN0 --> CC )   &    |- ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )   &    |- ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )   =>    |- ( ph -> ( F oF + G ) = ( z e. CC |-> sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) ) )
Theorem	plymullem1 15092*	Derive the coefficient function for the product of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> B : NN0 --> CC )   &    |- ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )   &    |- ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )   =>    |- ( ph -> ( F oF x. G ) = ( z e. CC |-> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) ) )
Theorem	plyaddlem 15093*	Lemma for plyadd 15095. (Contributed by Mario Carneiro, 21-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )   &    |- ( ph -> B e. ( ( S u. { 0 } ) ^m NN0 ) )   &    |- ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )   &    |- ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )   =>    |- ( ph -> ( F oF + G ) e. (Poly ` S ) )
Theorem	plymullem 15094*	Lemma for plymul 15096. (Contributed by Mario Carneiro, 21-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )   &    |- ( ph -> B e. ( ( S u. { 0 } ) ^m NN0 ) )   &    |- ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )   &    |- ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   =>    |- ( ph -> ( F oF x. G ) e. (Poly ` S ) )
Theorem	plyadd 15095*	The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   =>    |- ( ph -> ( F oF + G ) e. (Poly ` S ) )
Theorem	plymul 15096*	The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   =>    |- ( ph -> ( F oF x. G ) e. (Poly ` S ) )
Theorem	plysub 15097*	The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> -u 1 e. S )   =>    |- ( ph -> ( F oF - G ) e. (Poly ` S ) )
Theorem	plyaddcl 15098	The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> ( F oF + G ) e. (Poly ` CC ) )
Theorem	plymulcl 15099	The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> ( F oF x. G ) e. (Poly ` CC ) )
Theorem	plysubcl 15100	The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> ( F oF - G ) e. (Poly ` CC ) )