P. 156 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15501-15600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvfre 15501	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 15502*	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 15503*	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 15504*	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 15505	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 15506*	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 15507*	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 15508*	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 15509*	Closure lemma for dvmptmulx 15511 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 15510*	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 15511*	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 15512*	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 15513*	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 15514*	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 15515*	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 15516*	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 15517	Derivative of the exponential function at 0. The key step in the proof is eftlub 12312, 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 15518	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 15519	Extend class notation to include the set of complex polynomials.
class Poly
Syntax	cidp 15520	Extend class notation to include the identity polynomial.
class Xp
Definition	df-ply 15521*	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 15522	Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- Xp = ( _I |` CC )
Theorem	plyval 15523*	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 15524	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 15525*	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 15526*	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 15527	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 15528	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 15529	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 15530	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 15531*	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 15532*	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 15533*	Lemma for ply1term 15534. (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 15534*	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 15535*	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 15536	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 15537	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 15538*	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 15539*	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 15540*	Lemma for plyadd 15542. (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 15541*	Lemma for plymul 15543. (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 15542*	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 15543*	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 15544*	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 15545	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 15546	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 15547	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 15548*	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 15549*	Lemma for plyco 15550. 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 15550*	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 15551*	Lemma for plycj 15552. (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 15552*	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 15553	A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 8198. (Revised by GG, 16-Mar-2025.)
|- ( F e. (Poly ` S ) -> F e. ( CC -cn-> CC ) )
Theorem	plyrecj 15554	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 15555	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 15556*	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 15557	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 15558	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 15559	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 15560	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- sin e. ( CC -cn-> CC )
Theorem	coscn 15561	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- cos e. ( CC -cn-> CC )
Theorem	reeff1olem 15562*	Lemma for reeff1o 15564. (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 15563*	Lemma for reeff1o 15564. (Contributed by Jim Kingdon, 15-May-2024.)
|- ( U e. ( 0 (,) _e ) -> E. x e. RR ( exp ` x ) = U )
Theorem	reeff1o 15564	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 15565	Lemma for eflt 15566. The converse of efltim 12320 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 15566	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 15567	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 15568	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 15569	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 15570	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 15571	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 15572*	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 15573*	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 15574	Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )
Theorem	pigt2lt4 15575	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 15576	The sine of pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` pi ) = 0
Theorem	pire 15577	pi is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
|- pi e. RR
Theorem	picn 15578	pi is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- pi e. CC
Theorem	pipos 15579	pi is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- 0 < pi
Theorem	pirp 15580	pi is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- pi e. RR+
Theorem	negpicn 15581	-u pi is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u pi e. CC
Theorem	sinhalfpilem 15582	Lemma for sinhalfpi 15587 and coshalfpi 15588. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( ( sin ` ( pi / 2 ) ) = 1 /\ ( cos ` ( pi / 2 ) ) = 0 )
Theorem	halfpire 15583	pi / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
|- ( pi / 2 ) e. RR
Theorem	neghalfpire 15584	-u pi / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR
Theorem	neghalfpirx 15585	-u pi / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR*
Theorem	pidiv2halves 15586	Adding pi / 2 to itself gives pi. See 2halves 9416. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
Theorem	sinhalfpi 15587	The sine of pi / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( pi / 2 ) ) = 1
Theorem	coshalfpi 15588	The cosine of pi / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( pi / 2 ) ) = 0
Theorem	cosneghalfpi 15589	The cosine of -u pi / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
|- ( cos ` -u ( pi / 2 ) ) = 0
Theorem	efhalfpi 15590	The exponential of _i pi / 2 is _i. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( pi / 2 ) ) ) = _i
Theorem	cospi 15591	The cosine of pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` pi ) = -u 1
Theorem	efipi 15592	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 15593	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 15594	The sine of 2 pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( 2 x. pi ) ) = 0
Theorem	cos2pi 15595	The cosine of 2 pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( 2 x. pi ) ) = 1
Theorem	ef2pi 15596	The exponential of 2 pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( 2 x. pi ) ) ) = 1
Theorem	ef2kpi 15597	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 15598	The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( A + ( ( _i x. ( 2 x. pi ) ) x. K ) ) ) = ( exp ` A ) )
Theorem	sinperlem 15599	Lemma for sinper 15600 and cosper 15601. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( A e. CC -> ( F ` A ) = ( ( ( exp ` ( _i x. A ) ) O ( exp ` ( -u _i x. A ) ) ) / D ) )   &    |- ( ( A + ( K x. ( 2 x. pi ) ) ) e. CC -> ( F ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( ( ( exp ` ( _i x. ( A + ( K x. ( 2 x. pi ) ) ) ) ) O ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. pi ) ) ) ) ) ) / D ) )   =>    |- ( ( A e. CC /\ K e. ZZ ) -> ( F ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( F ` A ) )
Theorem	sinper 15600	The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( sin ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( sin ` A ) )