P. 160 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15901-16000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvcj 15901	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 15900. (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 15902	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 15903*	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 15904*	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 15905*	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 15906	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 15907*	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 15908*	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 15909*	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 15910*	Closure lemma for dvmptmulx 15912 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 15911*	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 15912*	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 15913*	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 15914*	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 15915*	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 15916*	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 15917*	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 15918	Derivative of the exponential function at 0. The key step in the proof is eftlub 12476, 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 15919	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 15920	Extend class notation to include the set of complex polynomials.
class Poly
Syntax	cidp 15921	Extend class notation to include the identity polynomial.
class Xp
Definition	df-ply 15922*	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 15923	Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- Xp = ( _I |` CC )
Theorem	plyval 15924*	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 15925	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 15926*	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 15927*	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 15928	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 15929	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 15930	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 15931	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 15932*	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 15933*	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 15934*	Lemma for ply1term 15935. (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 15935*	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 15936*	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 15937	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 15938	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 15939*	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 15940*	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 15941*	Lemma for plyadd 15943. (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 15942*	Lemma for plymul 15944. (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 15943*	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 15944*	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 15945*	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 15946	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 15947	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 15948	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 15949*	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 15950*	Lemma for plyco 15951. 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 15951*	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 15952*	Lemma for plycj 15953. (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 15953*	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 15954	A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 8303. (Revised by GG, 16-Mar-2025.)
|- ( F e. (Poly ` S ) -> F e. ( CC -cn-> CC ) )
Theorem	plyrecj 15955	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 15956	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 15957*	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 15958	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 15959	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 15960	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 15961	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- sin e. ( CC -cn-> CC )
Theorem	coscn 15962	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- cos e. ( CC -cn-> CC )
Theorem	reeff1olem 15963*	Lemma for reeff1o 15965. (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 15964*	Lemma for reeff1o 15965. (Contributed by Jim Kingdon, 15-May-2024.)
|- ( U e. ( 0 (,) _e ) -> E. x e. RR ( exp ` x ) = U )
Theorem	reeff1o 15965	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 15966	Lemma for eflt 15967. The converse of efltim 12484 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 15967	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 15968	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 15969	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 15970	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 ) ) )
Theorem	efap1p 15971	If the exponential of a number is apart from one plus that number, the number is apart from zero. To some extent can be thought of as the converse of efgt1p 12482. (Contributed by Jim Kingdon, 13-Aug-2026.)
|- ( ( A e. RR /\ ( 1 + A ) # ( exp ` A ) ) -> A # 0 )
11.2.2  Properties of pi = 3.14159...
Theorem	pilem1 15972	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 15973	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 15974*	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 15975*	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 15976	Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )
Theorem	pigt2lt4 15977	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 15978	The sine of pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` pi ) = 0
Theorem	pire 15979	pi is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
|- pi e. RR
Theorem	picn 15980	pi is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- pi e. CC
Theorem	pipos 15981	pi is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- 0 < pi
Theorem	pirp 15982	pi is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- pi e. RR+
Theorem	negpicn 15983	-u pi is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u pi e. CC
Theorem	sinhalfpilem 15984	Lemma for sinhalfpi 15989 and coshalfpi 15990. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( ( sin ` ( pi / 2 ) ) = 1 /\ ( cos ` ( pi / 2 ) ) = 0 )
Theorem	halfpire 15985	pi / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
|- ( pi / 2 ) e. RR
Theorem	neghalfpire 15986	-u pi / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR
Theorem	neghalfpirx 15987	-u pi / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR*
Theorem	pidiv2halves 15988	Adding pi / 2 to itself gives pi. See 2halves 9539. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
Theorem	sinhalfpi 15989	The sine of pi / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( pi / 2 ) ) = 1
Theorem	coshalfpi 15990	The cosine of pi / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( pi / 2 ) ) = 0
Theorem	cosneghalfpi 15991	The cosine of -u pi / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
|- ( cos ` -u ( pi / 2 ) ) = 0
Theorem	efhalfpi 15992	The exponential of _i pi / 2 is _i. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( pi / 2 ) ) ) = _i
Theorem	cospi 15993	The cosine of pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` pi ) = -u 1
Theorem	efipi 15994	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 15995	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 15996	The sine of 2 pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( 2 x. pi ) ) = 0
Theorem	cos2pi 15997	The cosine of 2 pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( 2 x. pi ) ) = 1
Theorem	ef2pi 15998	The exponential of 2 pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( 2 x. pi ) ) ) = 1
Theorem	ef2kpi 15999	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 16000	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 ) )