P. 202 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 20101-20200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dgrlem 20101*	Lemma for dgrcl 20105 and similar theorems. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   =>    |- ( F e. (Poly ` S ) -> ( A : NN0 --> ( S u. { 0 } ) /\ E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )
Theorem	coef 20102	The domain and range of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   =>    |- ( F e. (Poly ` S ) -> A : NN0 --> ( S u. { 0 } ) )
Theorem	coef2 20103	The domain and range of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   =>    |- ( ( F e. (Poly ` S ) /\ 0 e. S ) -> A : NN0 --> S )
Theorem	coef3 20104	The domain and range of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   =>    |- ( F e. (Poly ` S ) -> A : NN0 --> CC )
Theorem	dgrcl 20105	The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( F e. (Poly ` S ) -> (deg ` F ) e. NN0 )
Theorem	dgrub 20106	If the M-th coefficient of F is nonzero, then the degree of F is at least M. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   =>    |- ( ( F e. (Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> M <_ N )
Theorem	dgrub2 20107	All the coefficients above the degree of F are zero. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   =>    |- ( F e. (Poly ` S ) -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
Theorem	dgrlb 20108	If all the coefficients above M are zero, then the degree of F is at most M. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   =>    |- ( ( F e. (Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> N <_ M )
Theorem	coeidlem 20109*	Lemma for coeid 20110. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> B e. ( ( S u. { 0 } ) ^m NN0 ) )   &    |- ( ph -> ( B " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( B ` k ) x. ( z ^ k ) ) ) )   =>    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
Theorem	coeid 20110*	Reconstruct a polynomial as an explicit sum of the coefficient function up to the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   =>    |- ( F e. (Poly ` S ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
Theorem	coeid2 20111*	Reconstruct a polynomial as an explicit sum of the coefficient function up to the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   =>    |- ( ( F e. (Poly ` S ) /\ X e. CC ) -> ( F ` X ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( X ^ k ) ) )
Theorem	coeid3 20112*	Reconstruct a polynomial as an explicit sum of the coefficient function up to at least the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   =>    |- ( ( F e. (Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) -> ( F ` X ) = sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( X ^ k ) ) )
Theorem	plyco 20113*	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	coeeq2 20114*	Compute the coefficient function given a sum expression for the polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )   =>    |- ( ph -> (coeff ` F ) = ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) )
Theorem	dgrle 20115*	Given an explicit expression for a polynomial, the degree is at most the highest term in the sum. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )   =>    |- ( ph -> (deg ` F ) <_ N )
Theorem	dgreq 20116*	If the highest term in a polynomial expression is nonzero, then the polynomial's degree is completely determined. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> ( A ` N ) =/= 0 )   =>    |- ( ph -> (deg ` F ) = N )
Theorem	0dgr 20117	A constant function has degree 0. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( A e. CC -> (deg ` ( CC X. { A } ) ) = 0 )
Theorem	0dgrb 20118	A function has degree zero iff it is a constant function. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( F e. (Poly ` S ) -> ( (deg ` F ) = 0 <-> F = ( CC X. { ( F ` 0 ) } ) ) )
Theorem	coefv0 20119	The result of evaluating a polynomial at zero is the constant term. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- A = (coeff ` F )   =>    |- ( F e. (Poly ` S ) -> ( F ` 0 ) = ( A ` 0 ) )
Theorem	coeaddlem 20120	Lemma for coeadd 20122 and dgradd 20138. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- A = (coeff ` F )   &    |- B = (coeff ` G )   &    |- M = (deg ` F )   &    |- N = (deg ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> ( (coeff ` ( F o F + G ) ) = ( A o F + B ) /\ (deg ` ( F o F + G ) ) <_ if ( M <_ N , N , M ) ) )
Theorem	coemullem 20121*	Lemma for coemul 20123 and dgrmul 20141. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- A = (coeff ` F )   &    |- B = (coeff ` G )   &    |- M = (deg ` F )   &    |- N = (deg ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> ( (coeff ` ( F o F x. G ) ) = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) /\ (deg ` ( F o F x. G ) ) <_ ( M + N ) ) )
Theorem	coeadd 20122	The coefficient function of a sum is the sum of coefficients. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- A = (coeff ` F )   &    |- B = (coeff ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> (coeff ` ( F o F + G ) ) = ( A o F + B ) )
Theorem	coemul 20123*	A coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- A = (coeff ` F )   &    |- B = (coeff ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) /\ N e. NN0 ) -> ( (coeff ` ( F o F x. G ) ) ` N ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( B ` ( N - k ) ) ) )
Theorem	coe11 20124	The coefficient function is one-to-one, so if the coefficients are equal then the functions are equal and vice-versa. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- A = (coeff ` F )   &    |- B = (coeff ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> ( F = G <-> A = B ) )
Theorem	coemulhi 20125	The leading coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- A = (coeff ` F )   &    |- B = (coeff ` G )   &    |- M = (deg ` F )   &    |- N = (deg ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> ( (coeff ` ( F o F x. G ) ) ` ( M + N ) ) = ( ( A ` M ) x. ( B ` N ) ) )
Theorem	coemulc 20126	The coefficient function is linear under scalar multiplication. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( A e. CC /\ F e. (Poly ` S ) ) -> (coeff ` ( ( CC X. { A } ) o F x. F ) ) = ( ( NN0 X. { A } ) o F x. (coeff ` F ) ) )
Theorem	coe0 20127	The coefficients of the zero polynomial are zero. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- (coeff ` 0 p ) = ( NN0 X. { 0 } )
Theorem	coesub 20128	The coefficient function of a sum is the sum of coefficients. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- A = (coeff ` F )   &    |- B = (coeff ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> (coeff ` ( F o F - G ) ) = ( A o F - B ) )
Theorem	coe1termlem 20129*	The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- F = ( z e. CC |-> ( A x. ( z ^ N ) ) )   =>    |- ( ( A e. CC /\ N e. NN0 ) -> ( (coeff ` F ) = ( n e. NN0 |-> if ( n = N , A , 0 ) ) /\ ( A =/= 0 -> (deg ` F ) = N ) ) )
Theorem	coe1term 20130*	The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- F = ( z e. CC |-> ( A x. ( z ^ N ) ) )   =>    |- ( ( A e. CC /\ N e. NN0 /\ M e. NN0 ) -> ( (coeff ` F ) ` M ) = if ( M = N , A , 0 ) )
Theorem	dgr1term 20131*	The degree of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- F = ( z e. CC |-> ( A x. ( z ^ N ) ) )   =>    |- ( ( A e. CC /\ A =/= 0 /\ N e. NN0 ) -> (deg ` F ) = N )
Theorem	plycn 20132	A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( F e. (Poly ` S ) -> F e. ( CC -cn-> CC ) )
Theorem	dgr0 20133	The degree of the zero polynomial is zero. Note: this differs from some other definitions of the degree of the zero polynomial, such as -u 1 , -oo or undefined. But it is convenient for us to define it this way, so that we have dgrcl 20105, dgreq0 20136 and coeid 20110 without having to special-case zero, although plydivalg 20169 is a little more complicated as a result. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- (deg ` 0 p ) = 0
Theorem	coeidp 20134	The coefficients of the identity function. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( A e. NN0 -> ( (coeff ` X p ) ` A ) = if ( A = 1 , 1 , 0 ) )
Theorem	dgrid 20135	The degree of the identity function. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- (deg ` X p ) = 1
Theorem	dgreq0 20136	The leading coefficient of a polynomial is nonzero, unless the entire polynomial is zero. (Contributed by Mario Carneiro, 22-Jul-2014.) (Proof shortened by Fan Zheng, 21-Jun-2016.)
|- N = (deg ` F )   &    |- A = (coeff ` F )   =>    |- ( F e. (Poly ` S ) -> ( F = 0 p <-> ( A ` N ) = 0 ) )
Theorem	dgrlt 20137	Two ways to say that the degree of F is strictly less than N. (Contributed by Mario Carneiro, 25-Jul-2014.)
|- N = (deg ` F )   &    |- A = (coeff ` F )   =>    |- ( ( F e. (Poly ` S ) /\ M e. NN0 ) -> ( ( F = 0 p \/ N < M ) <-> ( N <_ M /\ ( A ` M ) = 0 ) ) )
Theorem	dgradd 20138	The degree of a sum of polynomials is at most the maximum of the degrees. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- M = (deg ` F )   &    |- N = (deg ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> (deg ` ( F o F + G ) ) <_ if ( M <_ N , N , M ) )
Theorem	dgradd2 20139	The degree of a sum of polynomials of unequal degrees is the degree of the larger polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- M = (deg ` F )   &    |- N = (deg ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) /\ M < N ) -> (deg ` ( F o F + G ) ) = N )
Theorem	dgrmul2 20140	The degree of a product of polynomials is at most the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- M = (deg ` F )   &    |- N = (deg ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> (deg ` ( F o F x. G ) ) <_ ( M + N ) )
Theorem	dgrmul 20141	The degree of a product of nonzero polynomials is the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- M = (deg ` F )   &    |- N = (deg ` G )   =>    |- ( ( ( F e. (Poly ` S ) /\ F =/= 0 p ) /\ ( G e. (Poly ` S ) /\ G =/= 0 p ) ) -> (deg ` ( F o F x. G ) ) = ( M + N ) )
Theorem	dgrmulc 20142	Scalar multiplication by a nonzero constant does not change the degree of a function. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( A e. CC /\ A =/= 0 /\ F e. (Poly ` S ) ) -> (deg ` ( ( CC X. { A } ) o F x. F ) ) = (deg ` F ) )
Theorem	dgrsub 20143	The degree of a difference of polynomials is at most the maximum of the degrees. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- M = (deg ` F )   &    |- N = (deg ` G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> (deg ` ( F o F - G ) ) <_ if ( M <_ N , N , M ) )
Theorem	dgrcolem1 20144*	The degree of a composition of a monomial with a polynomial. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- N = (deg ` G )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> G e. (Poly ` S ) )   =>    |- ( ph -> (deg ` ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) = ( M x. N ) )
Theorem	dgrcolem2 20145*	Lemma for dgrco 20146. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- M = (deg ` F )   &    |- N = (deg ` G )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- A = (coeff ` F )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> M = ( D + 1 ) )   &    |- ( ph -> A. f e. (Poly ` CC ) ( (deg ` f ) <_ D -> (deg ` ( f o. G ) ) = ( (deg ` f ) x. N ) ) )   =>    |- ( ph -> (deg ` ( F o. G ) ) = ( M x. N ) )
Theorem	dgrco 20146	The degree of a composition of two polynomials is the product of the degrees. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- M = (deg ` F )   &    |- N = (deg ` G )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   =>    |- ( ph -> (deg ` ( F o. G ) ) = ( M x. N ) )
Theorem	plycjlem 20147*	Lemma for plycj 20148 and coecj 20149. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- N = (deg ` F )   &    |- G = ( ( * o. F ) o. * )   &    |- A = (coeff ` F )   =>    |- ( F e. (Poly ` S ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) ) )
Theorem	plycj 20148*	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.)
|- N = (deg ` F )   &    |- G = ( ( * o. F ) o. * )   &    |- ( ( ph /\ x e. S ) -> ( * ` x ) e. S )   &    |- ( ph -> F e. (Poly ` S ) )   =>    |- ( ph -> G e. (Poly ` S ) )
Theorem	coecj 20149	Double conjugation of a polynomial causes the coefficients to be conjugated. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- N = (deg ` F )   &    |- G = ( ( * o. F ) o. * )   &    |- A = (coeff ` F )   =>    |- ( F e. (Poly ` S ) -> (coeff ` G ) = ( * o. A ) )
Theorem	plyrecj 20150	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	plymul0or 20151	Polynomial multiplication has no zero divisors. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) ) -> ( ( F o F x. G ) = 0 p <-> ( F = 0 p \/ G = 0 p ) ) )
Theorem	ofmulrt 20152	The set of roots of a product is the union of the roots of the terms. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( `' ( F o F x. G ) " { 0 } ) = ( ( `' F " { 0 } ) u. ( `' G " { 0 } ) ) )
Theorem	plyreres 20153	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 20154*	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 20155	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.)
|- ( ( S e. (SubRing ` ℂfld ) /\ F e. (Poly ` S ) ) -> ( CC _D F ) e. (Poly ` S ) )
Theorem	dvply2 20156	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 ) )
Theorem	dvnply2 20157	Polynomials have polynomials as derivatives of all orders. (Contributed by Mario Carneiro, 1-Jan-2017.)
|- ( ( S e. (SubRing ` ℂfld ) /\ F e. (Poly ` S ) /\ N e. NN0 ) -> ( ( CC D n F ) ` N ) e. (Poly ` S ) )
Theorem	dvnply 20158	Polynomials have polynomials as derivatives of all orders. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
|- ( ( F e. (Poly ` S ) /\ N e. NN0 ) -> ( ( CC D n F ) ` N ) e. (Poly ` CC ) )
Theorem	plycpn 20159	Polynomials are smooth. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( F e. (Poly ` S ) -> F e. |^| ran ( C ^n ` CC ) )
13.1.5  The division algorithm for polynomials
Syntax	cquot 20160	Extend class notation to include the quotient of a polynomial division.
class quot
Definition	df-quot 20161*	Define the quotient function on polynomials. This is the q of the expression f = g x. q + r in the division algorithm. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- quot = ( f e. (Poly ` CC ) , g e. ( (Poly ` CC ) \ { 0 p } ) |-> ( iota_ q e. (Poly ` CC ) [. ( f o F - ( g o F x. q ) ) / r ]. ( r = 0 p \/ (deg ` r ) < (deg ` g ) ) ) )
Theorem	quotval 20162*	Value of the quotient function. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- R = ( F o F - ( G o F x. q ) )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) /\ G =/= 0 p ) -> ( F quot G ) = ( iota_ q e. (Poly ` CC ) ( R = 0 p \/ (deg ` R ) < (deg ` G ) ) ) )
Theorem	plydivlem1 20163*	Lemma for plydivalg 20169. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )   &    |- ( ph -> -u 1 e. S )   =>    |- ( ph -> 0 e. S )
Theorem	plydivlem2 20164*	Lemma for plydivalg 20169. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )   &    |- ( ph -> -u 1 e. S )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ph -> G =/= 0 p )   &    |- R = ( F o F - ( G o F x. q ) )   =>    |- ( ( ph /\ q e. (Poly ` S ) ) -> R e. (Poly ` S ) )
Theorem	plydivlem3 20165*	Lemma for plydivex 20167. Base case of induction. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )   &    |- ( ph -> -u 1 e. S )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ph -> G =/= 0 p )   &    |- R = ( F o F - ( G o F x. q ) )   &    |- ( ph -> ( F = 0 p \/ ( (deg ` F ) - (deg ` G ) ) < 0 ) )   =>    |- ( ph -> E. q e. (Poly ` S ) ( R = 0 p \/ (deg ` R ) < (deg ` G ) ) )
Theorem	plydivlem4 20166*	Lemma for plydivex 20167. Induction step. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )   &    |- ( ph -> -u 1 e. S )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ph -> G =/= 0 p )   &    |- R = ( F o F - ( G o F x. q ) )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> ( M - N ) = D )   &    |- ( ph -> F =/= 0 p )   &    |- U = ( f o F - ( G o F x. p ) )   &    |- H = ( z e. CC |-> ( ( ( A ` M ) / ( B ` N ) ) x. ( z ^ D ) ) )   &    |- ( ph -> A. f e. (Poly ` S ) ( ( f = 0 p \/ ( (deg ` f ) - N ) < D ) -> E. p e. (Poly ` S ) ( U = 0 p \/ (deg ` U ) < N ) ) )   &    |- A = (coeff ` F )   &    |- B = (coeff ` G )   &    |- M = (deg ` F )   &    |- N = (deg ` G )   =>    |- ( ph -> E. q e. (Poly ` S ) ( R = 0 p \/ (deg ` R ) < N ) )
Theorem	plydivex 20167*	Lemma for plydivalg 20169. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )   &    |- ( ph -> -u 1 e. S )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ph -> G =/= 0 p )   &    |- R = ( F o F - ( G o F x. q ) )   =>    |- ( ph -> E. q e. (Poly ` S ) ( R = 0 p \/ (deg ` R ) < (deg ` G ) ) )
Theorem	plydiveu 20168*	Lemma for plydivalg 20169. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )   &    |- ( ph -> -u 1 e. S )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ph -> G =/= 0 p )   &    |- R = ( F o F - ( G o F x. q ) )   &    |- ( ph -> q e. (Poly ` S ) )   &    |- ( ph -> ( R = 0 p \/ (deg ` R ) < (deg ` G ) ) )   &    |- T = ( F o F - ( G o F x. p ) )   &    |- ( ph -> p e. (Poly ` S ) )   &    |- ( ph -> ( T = 0 p \/ (deg ` T ) < (deg ` G ) ) )   =>    |- ( ph -> p = q )
Theorem	plydivalg 20169*	The division algorithm on polynomials over a subfield S of the complex numbers. If F and G =/= 0 are polynomials over S, then there is a unique quotient polynomial q such that the remainder F - G x. q is either zero or has degree less than G. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )   &    |- ( ph -> -u 1 e. S )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ph -> G =/= 0 p )   &    |- R = ( F o F - ( G o F x. q ) )   =>    |- ( ph -> E! q e. (Poly ` S ) ( R = 0 p \/ (deg ` R ) < (deg ` G ) ) )
Theorem	quotlem 20170*	Lemma for properties of the polynomial quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )   &    |- ( ph -> -u 1 e. S )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ph -> G =/= 0 p )   &    |- R = ( F o F - ( G o F x. ( F quot G ) ) )   =>    |- ( ph -> ( ( F quot G ) e. (Poly ` S ) /\ ( R = 0 p \/ (deg ` R ) < (deg ` G ) ) ) )
Theorem	quotcl 20171*	The quotient of two polynomials in a field S is also in the field. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )   &    |- ( ph -> -u 1 e. S )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ph -> G =/= 0 p )   =>    |- ( ph -> ( F quot G ) e. (Poly ` S ) )
Theorem	quotcl2 20172	Closure of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) /\ G =/= 0 p ) -> ( F quot G ) e. (Poly ` CC ) )
Theorem	quotdgr 20173	Remainder property of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- R = ( F o F - ( G o F x. ( F quot G ) ) )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) /\ G =/= 0 p ) -> ( R = 0 p \/ (deg ` R ) < (deg ` G ) ) )
Theorem	plyremlem 20174	Closure of a linear factor. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- G = ( X p o F - ( CC X. { A } ) )   =>    |- ( A e. CC -> ( G e. (Poly ` CC ) /\ (deg ` G ) = 1 /\ ( `' G " { 0 } ) = { A } ) )
Theorem	plyrem 20175	The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 12997). If a polynomial F is divided by the linear factor x - A, the remainder is equal to F ( A ), the evaluation of the polynomial at A (interpreted as a constant polynomial). (Contributed by Mario Carneiro, 26-Jul-2014.)
|- G = ( X p o F - ( CC X. { A } ) )   &    |- R = ( F o F - ( G o F x. ( F quot G ) ) )   =>    |- ( ( F e. (Poly ` S ) /\ A e. CC ) -> R = ( CC X. { ( F ` A ) } ) )
Theorem	facth 20176	The factor theorem. If a polynomial F has a root at A, then G = x - A is a factor of F (and the other factor is F quot G). (Contributed by Mario Carneiro, 26-Jul-2014.)
|- G = ( X p o F - ( CC X. { A } ) )   =>    |- ( ( F e. (Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> F = ( G o F x. ( F quot G ) ) )
Theorem	fta1lem 20177*	Lemma for fta1 20178. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- R = ( `' F " { 0 } )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> F e. ( (Poly ` CC ) \ { 0 p } ) )   &    |- ( ph -> (deg ` F ) = ( D + 1 ) )   &    |- ( ph -> A e. ( `' F " { 0 } ) )   &    |- ( ph -> A. g e. ( (Poly ` CC ) \ { 0 p } ) ( (deg ` g ) = D -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ (deg ` g ) ) ) )   =>    |- ( ph -> ( R e. Fin /\ ( # ` R ) <_ (deg ` F ) ) )
Theorem	fta1 20178	The easy direction of the Fundamental Theorem of Algebra: A nonzero polynomial has at most deg ( F ) roots. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- R = ( `' F " { 0 } )   =>    |- ( ( F e. (Poly ` S ) /\ F =/= 0 p ) -> ( R e. Fin /\ ( # ` R ) <_ (deg ` F ) ) )
Theorem	quotcan 20179	Exact division with a multiple. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- H = ( F o F x. G )   =>    |- ( ( F e. (Poly ` S ) /\ G e. (Poly ` S ) /\ G =/= 0 p ) -> ( H quot G ) = F )
Theorem	vieta1lem1 20180*	Lemma for vieta1 20182. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- R = ( `' F " { 0 } )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> ( # ` R ) = N )   &    |- ( ph -> D e. NN )   &    |- ( ph -> ( D + 1 ) = N )   &    |- ( ph -> A. f e. (Poly ` CC ) ( ( D = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) / ( (coeff ` f ) ` (deg ` f ) ) ) ) )   &    |- Q = ( F quot ( X p o F - ( CC X. { z } ) ) )   =>    |- ( ( ph /\ z e. R ) -> ( Q e. (Poly ` CC ) /\ D = (deg ` Q ) ) )
Theorem	vieta1lem2 20181*	Lemma for vieta1 20182: inductive step. Let z be a root of F. Then F = ( X p - z ) x. Q for some Q by the factor theorem, and Q is a degree- D polynomial, so by the induction hypothesis sum_ x e. ( `' Q " 0 ) x = -u (coeff ` Q ) ` ( D - 1 ) / (coeff ` Q ) ` D, so sum_ x e. R x = z - (coeff ` Q ) ` ( D - 1 ) / (coeff ` Q ) ` D. Now the coefficients of F are A ` ( D + 1 ) = (coeff ` Q ) ` D and A ` D = sum_ k e. ( 0 ... D ) (coeff ` X p - z ) ` k x. (coeff ` Q ) ` ( D - k ), which works out to -u z x. (coeff ` Q ) ` D + (coeff ` Q ) ` ( D - 1 ), so putting it all together we have sum_ x e. R x = -u A ` D / A ` ( D + 1 ) as we wanted to show. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- R = ( `' F " { 0 } )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> ( # ` R ) = N )   &    |- ( ph -> D e. NN )   &    |- ( ph -> ( D + 1 ) = N )   &    |- ( ph -> A. f e. (Poly ` CC ) ( ( D = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) / ( (coeff ` f ) ` (deg ` f ) ) ) ) )   &    |- Q = ( F quot ( X p o F - ( CC X. { z } ) ) )   =>    |- ( ph -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
Theorem	vieta1 20182*	The first-order Vieta's formula (see http://en.wikipedia.org/wiki/Vieta%27s_formulas). If a polynomial of degree N has N distinct roots, then the sum over these roots can be calculated as -u A ( N - 1 ) / A ( N ). (If the roots are not distinct, then this formula is still true but must double-count some of the roots according to their multiplicities.) (Contributed by Mario Carneiro, 28-Jul-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- R = ( `' F " { 0 } )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> ( # ` R ) = N )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
Theorem	plyexmo 20183*	An infinite set of values can be extended to a polynomial in at most one way. (Contributed by Stefan O'Rear, 14-Nov-2014.)
|- ( ( D C_ CC /\ -. D e. Fin ) -> E* p ( p e. (Poly ` S ) /\ ( p |` D ) = F ) )
13.1.6  Algebraic numbers
Syntax	caa 20184	Extend class notation to include the set of algebraic numbers.
class AA
Definition	df-aa 20185	Define the set of algebraic numbers. An algebraic number is a root of a nonzero polynomial over the integers. Here we construct it as the union of all kernels (preimages of { 0 }) of all polynomials in (Poly ` ZZ ), except the zero polynomial 0 p. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- AA = U_ f e. ( (Poly ` ZZ ) \ { 0 p } ) ( `' f " { 0 } )
Theorem	elaa 20186*	Elementhood in the set of algebraic numbers. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( A e. AA <-> ( A e. CC /\ E. f e. ( (Poly ` ZZ ) \ { 0 p } ) ( f ` A ) = 0 ) )
Theorem	aacn 20187	An algebraic number is a complex number. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( A e. AA -> A e. CC )
Theorem	aasscn 20188	The algebraic numbers are a subset of the complex numbers. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- AA C_ CC
Theorem	elqaalem1 20189*	Lemma for elqaa 20192. The function N represents the denominators of the rational coefficients B. By multiplying them all together to make R, we get a number big enough to clear all the denominators and make R x. F an integer polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> F e. ( (Poly ` QQ ) \ { 0 p } ) )   &    |- ( ph -> ( F ` A ) = 0 )   &    |- B = (coeff ` F )   &    |- N = ( k e. NN0 |-> sup ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , `' < ) )   &    |- R = ( seq 0 ( x. , N ) ` (deg ` F ) )   =>    |- ( ( ph /\ K e. NN0 ) -> ( ( N ` K ) e. NN /\ ( ( B ` K ) x. ( N ` K ) ) e. ZZ ) )
Theorem	elqaalem2 20190*	Lemma for elqaa 20192. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> F e. ( (Poly ` QQ ) \ { 0 p } ) )   &    |- ( ph -> ( F ` A ) = 0 )   &    |- B = (coeff ` F )   &    |- N = ( k e. NN0 |-> sup ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , `' < ) )   &    |- R = ( seq 0 ( x. , N ) ` (deg ` F ) )   &    |- P = ( x e. _V , y e. _V |-> ( ( x x. y ) mod ( N ` K ) ) )   =>    |- ( ( ph /\ K e. ( 0 ... (deg ` F ) ) ) -> ( R mod ( N ` K ) ) = 0 )
Theorem	elqaalem3 20191*	Lemma for elqaa 20192. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> F e. ( (Poly ` QQ ) \ { 0 p } ) )   &    |- ( ph -> ( F ` A ) = 0 )   &    |- B = (coeff ` F )   &    |- N = ( k e. NN0 |-> sup ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , `' < ) )   &    |- R = ( seq 0 ( x. , N ) ` (deg ` F ) )   =>    |- ( ph -> A e. AA )
Theorem	elqaa 20192*	The set of numbers generated by the roots of polynomials in the rational numbers is the same as the set of algebraic numbers, which by elaa 20186 are defined only in terms of polynomials over the integers. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( A e. AA <-> ( A e. CC /\ E. f e. ( (Poly ` QQ ) \ { 0 p } ) ( f ` A ) = 0 ) )
Theorem	qaa 20193	Every rational number is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( A e. QQ -> A e. AA )
Theorem	qssaa 20194	The rational numbers are contained in the algebraic numbers. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- QQ C_ AA
Theorem	iaa 20195	The imaginary unit is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- _i e. AA
Theorem	aareccl 20196	The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( A e. AA /\ A =/= 0 ) -> ( 1 / A ) e. AA )
Theorem	aacjcl 20197	The conjugate of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( A e. AA -> ( * ` A ) e. AA )
Theorem	aannenlem1 20198*	Lemma for aannen 20201. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- H = ( a e. NN0 |-> { b e. CC | E. c e. { d e. (Poly ` ZZ ) | ( d =/= 0 p /\ (deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( (coeff ` d ) ` e ) ) <_ a ) } ( c ` b ) = 0 } )   =>    |- ( A e. NN0 -> ( H ` A ) e. Fin )
Theorem	aannenlem2 20199*	Lemma for aannen 20201. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- H = ( a e. NN0 |-> { b e. CC | E. c e. { d e. (Poly ` ZZ ) | ( d =/= 0 p /\ (deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( (coeff ` d ) ` e ) ) <_ a ) } ( c ` b ) = 0 } )   =>    |- AA = U. ran H
Theorem	aannenlem3 20200*	The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- H = ( a e. NN0 |-> { b e. CC | E. c e. { d e. (Poly ` ZZ ) | ( d =/= 0 p /\ (deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( (coeff ` d ) ` e ) ) <_ a ) } ( c ` b ) = 0 } )   =>    |- AA ~~ NN