P. 155 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15401-15500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvbssntrcntop 15401	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 15402	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 15403	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 15404	Both RR and CC are subsets of CC. (Contributed by Mario Carneiro, 10-Feb-2015.)
|- ( S e. { RR , CC } -> S C_ CC )
Theorem	dvfgg 15405	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 15406	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 15407	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 15408*	Lemma for dvid 15412 and dvconst 15411. (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 15409*	Lemma for dvidre 15414 and dvconstre 15413. Analogue of dvidlemap 15408 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 15410*	Lemma for dvconstss 15415. Analogue of dvidlemap 15408 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 15411	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 15412	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 15413	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 15414	Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( RR _D ( _I |` RR ) ) = ( RR X. { 1 } )
Theorem	dvconstss 15415	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 15416	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 15417	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 15418	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 15419	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 15421. (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 15420	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 15418. (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 15421	The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 15419. (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 15422	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 15423	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 15424*	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 15425	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 15426. (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 15426	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 15425. (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 15427	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 15428*	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 15429*	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 15430*	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 15431	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 15432*	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 15433*	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 15434*	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 15435*	Closure lemma for dvmptmulx 15437 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 15436*	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 15437*	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 15438*	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 15439*	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 15440*	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 15441*	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 15442*	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 15443	Derivative of the exponential function at 0. The key step in the proof is eftlub 12244, 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 15444	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 15445	Extend class notation to include the set of complex polynomials.
class Poly
Syntax	cidp 15446	Extend class notation to include the identity polynomial.
class Xp
Definition	df-ply 15447*	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 15448	Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- Xp = ( _I |` CC )
Theorem	plyval 15449*	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 15450	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 15451*	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 15452*	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 15453	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 15454	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 15455	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 15456	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 15457*	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 15458*	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 15459*	Lemma for ply1term 15460. (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 15460*	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 15461*	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 15462	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 15463	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 15464*	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 15465*	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 15466*	Lemma for plyadd 15468. (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 15467*	Lemma for plymul 15469. (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 15468*	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 15469*	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 15470*	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 15471	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 15472	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 15473	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 ) )
Theorem	plycoeid3 15474*	Reconstruct a polynomial as an explicit sum of the coefficient function up to an index no smaller than the degree of the polynomial. (Contributed by Jim Kingdon, 17-Oct-2025.)
|- ( ph -> D e. NN0 )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> ( A " ( ZZ>= ` ( D + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... D ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> M e. ( ZZ>= ` D ) )   &    |- ( ph -> X e. CC )   =>    |- ( ph -> ( F ` X ) = sum_ j e. ( 0 ... M ) ( ( A ` j ) x. ( X ^ j ) ) )
Theorem	plycolemc 15475*	Lemma for plyco 15476. The result expressed as a sum, with a degree and coefficients for F specified as hypotheses. (Contributed by Jim Kingdon, 20-Sep-2025.)
|- ( 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 -> N e. NN0 )   &    |- ( ph -> A : NN0 --> ( S u. { 0 } ) )   &    |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( x e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) ) )   =>    |- ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( G ` z ) ^ k ) ) ) e. (Poly ` S ) )
Theorem	plyco 15476*	The composition of two polynomials is a polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-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 o. G ) e. (Poly ` S ) )
Theorem	plycjlemc 15477*	Lemma for plycj 15478. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.)
|- ( ph -> N e. NN0 )   &    |- G = ( ( * o. F ) o. * )   &    |- ( ph -> A : NN0 --> ( S u. { 0 } ) )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> F e. (Poly ` S ) )   =>    |- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) ) )
Theorem	plycj 15478*	The double conjugation of a polynomial is a polynomial. (The single conjugation is not because our definition of polynomial includes only holomorphic functions, i.e. no dependence on ( * ` z ) independently of z.) (Contributed by Mario Carneiro, 24-Jul-2014.)
|- G = ( ( * o. F ) o. * )   &    |- ( ( ph /\ x e. S ) -> ( * ` x ) e. S )   &    |- ( ph -> F e. (Poly ` S ) )   =>    |- ( ph -> G e. (Poly ` S ) )
Theorem	plycn 15479	A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 8148. (Revised by GG, 16-Mar-2025.)
|- ( F e. (Poly ` S ) -> F e. ( CC -cn-> CC ) )
Theorem	plyrecj 15480	A polynomial with real coefficients distributes under conjugation. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( F e. (Poly ` RR ) /\ A e. CC ) -> ( * ` ( F ` A ) ) = ( F ` ( * ` A ) ) )
Theorem	plyreres 15481	Real-coefficient polynomials restrict to real functions. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( F e. (Poly ` RR ) -> ( F |` RR ) : RR --> RR )
Theorem	dvply1 15482*	Derivative of a polynomial, explicit sum version. (Contributed by Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- B = ( k e. NN0 |-> ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( CC _D F ) = G )
Theorem	dvply2g 15483	The derivative of a polynomial with coefficients in a subring is a polynomial with coefficients in the same ring. (Contributed by Mario Carneiro, 1-Jan-2017.) (Revised by GG, 30-Apr-2025.)
|- ( ( S e. (SubRing ` ℂfld ) /\ F e. (Poly ` S ) ) -> ( CC _D F ) e. (Poly ` S ) )
Theorem	dvply2 15484	The derivative of a polynomial is a polynomial. (Contributed by Stefan O'Rear, 14-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
|- ( F e. (Poly ` S ) -> ( CC _D F ) e. (Poly ` CC ) )
11.2  Basic trigonometry
11.2.1  The exponential, sine, and cosine functions (cont.)
Theorem	efcn 15485	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 15486	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- sin e. ( CC -cn-> CC )
Theorem	coscn 15487	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- cos e. ( CC -cn-> CC )
Theorem	reeff1olem 15488*	Lemma for reeff1o 15490. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( ( U e. RR /\ 1 < U ) -> E. x e. RR ( exp ` x ) = U )
Theorem	reeff1oleme 15489*	Lemma for reeff1o 15490. (Contributed by Jim Kingdon, 15-May-2024.)
|- ( U e. ( 0 (,) _e ) -> E. x e. RR ( exp ` x ) = U )
Theorem	reeff1o 15490	The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
|- ( exp |` RR ) : RR -1-1-onto-> RR+
Theorem	efltlemlt 15491	Lemma for eflt 15492. The converse of efltim 12252 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( exp ` A ) < ( exp ` B ) )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> ( ( abs ` ( A - B ) ) < D -> ( abs ` ( ( exp ` A ) - ( exp ` B ) ) ) < ( ( exp ` B ) - ( exp ` A ) ) ) )   =>    |- ( ph -> A < B )
Theorem	eflt 15492	The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 21-May-2024.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( exp ` A ) < ( exp ` B ) ) )
Theorem	efle 15493	The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( exp ` A ) <_ ( exp ` B ) ) )
Theorem	reefiso 15494	The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) (Revised by Mario Carneiro, 11-Mar-2014.)
|- ( exp |` RR ) Isom < , < ( RR , RR+ )
Theorem	reapef 15495	Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.)
|- ( ( A e. RR /\ B e. RR ) -> ( A # B <-> ( exp ` A ) # ( exp ` B ) ) )
11.2.2  Properties of pi = 3.14159...
Theorem	pilem1 15496	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 15497	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 15498*	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 15499*	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 15500	Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )