P. 240 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23901-24000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mon1pval 23901*	Value of the set of monic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` P )   &    |- D = ( deg1 ` R )   &    |- M = (Monic1p ` R )   &    |- .1. = ( 1r ` R )   =>    |- M = { f e. B | ( f =/= .0. /\ ( (coe1 ` f ) ` ( D ` f ) ) = .1. ) }
Theorem	ismon1p 23902	Being a monic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` P )   &    |- D = ( deg1 ` R )   &    |- M = (Monic1p ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( F e. M <-> ( F e. B /\ F =/= .0. /\ ( (coe1 ` F ) ` ( D ` F ) ) = .1. ) )
Theorem	uc1pcl 23903	Unitic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   =>    |- ( F e. C -> F e. B )
Theorem	mon1pcl 23904	Monic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- M = (Monic1p ` R )   =>    |- ( F e. M -> F e. B )
Theorem	uc1pn0 23905	Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- C = (Unic1p ` R )   =>    |- ( F e. C -> F =/= .0. )
Theorem	mon1pn0 23906	Monic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- M = (Monic1p ` R )   =>    |- ( F e. M -> F =/= .0. )
Theorem	uc1pdeg 23907	Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- C = (Unic1p ` R )   =>    |- ( ( R e. Ring /\ F e. C ) -> ( D ` F ) e. NN0 )
Theorem	uc1pldg 23908	Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- U = (Unit ` R )   &    |- C = (Unic1p ` R )   =>    |- ( F e. C -> ( (coe1 ` F ) ` ( D ` F ) ) e. U )
Theorem	mon1pldg 23909	Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- .1. = ( 1r ` R )   &    |- M = (Monic1p ` R )   =>    |- ( F e. M -> ( (coe1 ` F ) ` ( D ` F ) ) = .1. )
Theorem	mon1puc1p 23910	Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- C = (Unic1p ` R )   &    |- M = (Monic1p ` R )   =>    |- ( ( R e. Ring /\ X e. M ) -> X e. C )
Theorem	uc1pmon1p 23911	Make a unitic polynomial monic by multiplying a factor to normalize the leading coefficient. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- C = (Unic1p ` R )   &    |- M = (Monic1p ` R )   &    |- P = (Poly1 ` R )   &    |- .x. = ( .r ` P )   &    |- A = (algSc ` P )   &    |- D = ( deg1 ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. C ) -> ( ( A ` ( I ` ( (coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) e. M )
Theorem	deg1submon1p 23912	The difference of two monic polynomials of the same degree is a polynomial of lesser degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- O = (Monic1p ` R )   &    |- P = (Poly1 ` R )   &    |- .- = ( -g ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. O )   &    |- ( ph -> ( D ` F ) = X )   &    |- ( ph -> G e. O )   &    |- ( ph -> ( D ` G ) = X )   =>    |- ( ph -> ( D ` ( F .- G ) ) < X )
Theorem	q1pval 23913*	Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Q = (quot1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- .- = ( -g ` P )   &    |- .x. = ( .r ` P )   =>    |- ( ( F e. B /\ G e. B ) -> ( F Q G ) = ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
Theorem	q1peqb 23914	Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Q = (quot1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- .- = ( -g ` P )   &    |- .x. = ( .r ` P )   &    |- C = (Unic1p ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) <-> ( F Q G ) = X ) )
Theorem	q1pcl 23915	Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Q = (quot1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F Q G ) e. B )
Theorem	r1pval 23916	Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- E = (rem1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- Q = (quot1p ` R )   &    |- .x. = ( .r ` P )   &    |- .- = ( -g ` P )   =>    |- ( ( F e. B /\ G e. B ) -> ( F E G ) = ( F .- ( ( F Q G ) .x. G ) ) )
Theorem	r1pcl 23917	Closure of remainder following division by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- E = (rem1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F E G ) e. B )
Theorem	r1pdeglt 23918	The remainder has a degree smaller than the divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- E = (rem1p ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   &    |- D = ( deg1 ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( D ` ( F E G ) ) < ( D ` G ) )
Theorem	r1pid 23919	Express the original polynomial F as F = ( q x. G ) + r using the quotient and remainder functions for q and r. (Contributed by Mario Carneiro, 5-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   &    |- Q = (quot1p ` R )   &    |- E = (rem1p ` R )   &    |- .x. = ( .r ` P )   &    |- .+ = ( +g ` P )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> F = ( ( ( F Q G ) .x. G ) .+ ( F E G ) ) )
Theorem	dvdsq1p 23920	Divisibility in a polynomial ring is witnessed by the quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- .|| = ( ||r ` P )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   &    |- .x. = ( .r ` P )   &    |- Q = (quot1p ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( G .|| F <-> F = ( ( F Q G ) .x. G ) ) )
Theorem	dvdsr1p 23921	Divisibility in a polynomial ring in terms of the remainder. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- .|| = ( ||r ` P )   &    |- B = ( Base ` P )   &    |- C = (Unic1p ` R )   &    |- .0. = ( 0g ` P )   &    |- E = (rem1p ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( G .|| F <-> ( F E G ) = .0. ) )
Theorem	ply1remlem 23922	A term of the form x - N is linear, monic, and has exactly one zero. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` N ) )   &    |- O = (eval1 ` R )   &    |- ( ph -> R e. NzRing )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. K )   &    |- U = (Monic1p ` R )   &    |- D = ( deg1 ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ph -> ( G e. U /\ ( D ` G ) = 1 /\ ( `' ( O ` G ) " { .0. } ) = { N } ) )
Theorem	ply1rem 23923	The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 15260). 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, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` N ) )   &    |- O = (eval1 ` R )   &    |- ( ph -> R e. NzRing )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. K )   &    |- ( ph -> F e. B )   &    |- E = (rem1p ` R )   =>    |- ( ph -> ( F E G ) = ( A ` ( ( O ` F ) ` N ) ) )
Theorem	facth1 23924	The factor theorem and its converse. A polynomial F has a root at A iff G = x - A is a factor of F. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` N ) )   &    |- O = (eval1 ` R )   &    |- ( ph -> R e. NzRing )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. K )   &    |- ( ph -> F e. B )   &    |- .0. = ( 0g ` R )   &    |- .|| = ( ||r ` P )   =>    |- ( ph -> ( G .|| F <-> ( ( O ` F ) ` N ) = .0. ) )
Theorem	fta1glem1 23925	Lemma for fta1g 23927. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- O = (eval1 ` R )   &    |- W = ( 0g ` R )   &    |- .0. = ( 0g ` P )   &    |- ( ph -> R e. IDomn )   &    |- ( ph -> F e. B )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` T ) )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> ( D ` F ) = ( N + 1 ) )   &    |- ( ph -> T e. ( `' ( O ` F ) " { W } ) )   =>    |- ( ph -> ( D ` ( F (quot1p ` R ) G ) ) = N )
Theorem	fta1glem2 23926*	Lemma for fta1g 23927. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- O = (eval1 ` R )   &    |- W = ( 0g ` R )   &    |- .0. = ( 0g ` P )   &    |- ( ph -> R e. IDomn )   &    |- ( ph -> F e. B )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` T ) )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> ( D ` F ) = ( N + 1 ) )   &    |- ( ph -> T e. ( `' ( O ` F ) " { W } ) )   &    |- ( ph -> A. g e. B ( ( D ` g ) = N -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) )   =>    |- ( ph -> ( # ` ( `' ( O ` F ) " { W } ) ) <_ ( D ` F ) )
Theorem	fta1g 23927	The one-sided fundamental theorem of algebra. A polynomial of degree n has at most n roots. Unlike the real fundamental theorem fta 24806, which is only true in CC and other algebraically closed fields, this is true in any integral domain. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- O = (eval1 ` R )   &    |- W = ( 0g ` R )   &    |- .0. = ( 0g ` P )   &    |- ( ph -> R e. IDomn )   &    |- ( ph -> F e. B )   &    |- ( ph -> F =/= .0. )   =>    |- ( ph -> ( # ` ( `' ( O ` F ) " { W } ) ) <_ ( D ` F ) )
Theorem	fta1blem 23928	Lemma for fta1b 23929. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- O = (eval1 ` R )   &    |- W = ( 0g ` R )   &    |- .0. = ( 0g ` P )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> M e. K )   &    |- ( ph -> N e. K )   &    |- ( ph -> ( M .X. N ) = W )   &    |- ( ph -> M =/= W )   &    |- ( ph -> ( ( M .x. X ) e. ( B \ { .0. } ) -> ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <_ ( D ` ( M .x. X ) ) ) )   =>    |- ( ph -> N = W )
Theorem	fta1b 23929*	The assumption that R be a domain in fta1g 23927 is necessary. Here we show that the statement is strong enough to prove that R is a domain. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- D = ( deg1 ` R )   &    |- O = (eval1 ` R )   &    |- W = ( 0g ` R )   &    |- .0. = ( 0g ` P )   =>    |- ( R e. IDomn <-> ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) )
Theorem	drnguc1p 23930	Over a division ring, all nonzero polynomials are unitic. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` P )   &    |- C = (Unic1p ` R )   =>    |- ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> F e. C )
Theorem	ig1peu 23931*	There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- .0. = ( 0g ` P )   &    |- M = (Monic1p ` R )   &    |- D = ( deg1 ` R )   =>    |- ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> E! g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )
Theorem	ig1pval 23932*	Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- .0. = ( 0g ` P )   &    |- U = (LIdeal ` P )   &    |- D = ( deg1 ` R )   &    |- M = (Monic1p ` R )   =>    |- ( ( R e. V /\ I e. U ) -> ( G ` I ) = if ( I = { .0. } , .0. , ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) )
Theorem	ig1pval2 23933	Generator of the zero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- .0. = ( 0g ` P )   =>    |- ( R e. Ring -> ( G ` { .0. } ) = .0. )
Theorem	ig1pval3 23934	Characterizing properties of the monic generator of a nonzero ideal of polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- .0. = ( 0g ` P )   &    |- U = (LIdeal ` P )   &    |- D = ( deg1 ` R )   &    |- M = (Monic1p ` R )   =>    |- ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( ( G ` I ) e. I /\ ( G ` I ) e. M /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
Theorem	ig1pcl 23935	The monic generator of an ideal is always in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- U = (LIdeal ` P )   =>    |- ( ( R e. DivRing /\ I e. U ) -> ( G ` I ) e. I )
Theorem	ig1pdvds 23936	The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- U = (LIdeal ` P )   &    |- .|| = ( ||r ` P )   =>    |- ( ( R e. DivRing /\ I e. U /\ X e. I ) -> ( G ` I ) .|| X )
Theorem	ig1prsp 23937	Any ideal of polynomials over a division ring is generated by the ideal's canonical generator. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- U = (LIdeal ` P )   &    |- K = (RSpan ` P )   =>    |- ( ( R e. DivRing /\ I e. U ) -> I = ( K ` { ( G ` I ) } ) )
Theorem	ply1lpir 23938	The ring of polynomials over a division ring has the principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. DivRing -> P e. LPIR )
Theorem	ply1pid 23939	The polynomials over a field are a PID. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. Field -> P e. PID )
14.1.3  Elementary properties of complex polynomials
Syntax	cply 23940	Extend class notation to include the set of complex polynomials.
class Poly
Syntax	cidp 23941	Extend class notation to include the identity polynomial.
class Xp
Syntax	ccoe 23942	Extend class notation to include the coefficient function on polynomials.
class coeff
Syntax	cdgr 23943	Extend class notation to include the degree function on polynomials.
class deg
Definition	df-ply 23944*	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 23945	Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- Xp = ( _I |` CC )
Definition	df-coe 23946*	Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- coeff = ( f e. (Poly ` CC ) |-> ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
Definition	df-dgr 23947	Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- deg = ( f e. (Poly ` CC ) |-> sup ( ( `' (coeff ` f ) " ( CC \ { 0 } ) ) , NN0 , < ) )
Theorem	plyco0 23948*	Two ways to say that a function on the nonnegative integers has finite support. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
Theorem	plyval 23949*	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 23950	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 23951*	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 23952*	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 23953	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 23954	The polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( F e. (Poly ` S ) -> F : CC --> CC )
Theorem	plyss 23955	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 23956	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 23957*	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 23958*	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 23959*	Lemma for ply1term 23960. (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 23960*	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 23961*	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 23962	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	ne0p 23963	A test to show that a polynomial is nonzero. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( ( A e. CC /\ ( F ` A ) =/= 0 ) -> F =/= 0p )
Theorem	ply0 23964	The zero function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- ( S C_ CC -> 0p e. (Poly ` S ) )
Theorem	plyid 23965	The identity function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
|- ( ( S C_ CC /\ 1 e. S ) -> Xp e. (Poly ` S ) )
Theorem	plyeq0lem 23966*	Lemma for plyeq0 23967. If A is the coefficient function for a nonzero polynomial such that P ( z ) = sum_ k e. NN0 A ( k ) x. z ^ k = 0 for every z e. CC and A ( M ) is the nonzero leading coefficient, then the function F ( z ) = P ( z ) / z ^ M is a sum of powers of 1 / z, and so the limit of this function as z ~~> +oo is the constant term, A ( M ). But F ( z ) = 0 everywhere, so this limit is also equal to zero so that A ( M ) = 0, a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( ph -> S C_ CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )   &    |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> 0p = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- M = sup ( ( `' A " ( S \ { 0 } ) ) , RR , < )   &    |- ( ph -> ( `' A " ( S \ { 0 } ) ) =/= (/) )   =>    |- -. ph
Theorem	plyeq0 23967*	If a polynomial is zero at every point (or even just zero at the positive integers), then all the coefficients must be zero. This is the basis for the method of equating coefficients of equal polynomials, and ensures that df-coe 23946 is well-defined. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( ph -> S C_ CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )   &    |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> 0p = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )   =>    |- ( ph -> A = ( NN0 X. { 0 } ) )
Theorem	plypf1 23968	Write the set of complex polynomials in a subring in terms of the abstract polynomial construction. (Contributed by Mario Carneiro, 3-Jul-2015.) (Proof shortened by AV, 29-Sep-2019.)
|- R = (ℂfld ↾s S )   &    |- P = (Poly1 ` R )   &    |- A = ( Base ` P )   &    |- E = (eval1 ` ℂfld )   =>    |- ( S e. (SubRing ` ℂfld ) -> (Poly ` S ) = ( E " A ) )
Theorem	plyaddlem1 23969*	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 23970*	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 23971*	Lemma for plyadd 23973. (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 23972*	Lemma for plymul 23974. (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 23973*	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 23974*	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 23975*	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 23976	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 23977	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 23978	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	coeval 23979*	Value of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( F e. (Poly ` S ) -> (coeff ` F ) = ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
Theorem	coeeulem 23980*	Lemma for coeeu 23981. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> A e. ( CC ^m NN0 ) )   &    |- ( ph -> B e. ( CC ^m NN0 ) )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. 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 -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )   =>    |- ( ph -> A = B )
Theorem	coeeu 23981*	Uniqueness of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( F e. (Poly ` S ) -> E! a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
Theorem	coelem 23982*	Lemma for properties of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( F e. (Poly ` S ) -> ( (coeff ` F ) e. ( CC ^m NN0 ) /\ E. n e. NN0 ( ( (coeff ` F ) " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( (coeff ` F ) ` k ) x. ( z ^ k ) ) ) ) ) )
Theorem	coeeq 23983*	If A satisfies the properties of the coefficient function, it must be equal to the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-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 -> (coeff ` F ) = A )
Theorem	dgrval 23984	Value of the degree function. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- A = (coeff ` F )   =>    |- ( F e. (Poly ` S ) -> (deg ` F ) = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
Theorem	dgrlem 23985*	Lemma for dgrcl 23989 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 23986	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 23987	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 23988	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 23989	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 23990	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 23991	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 23992	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 23993*	Lemma for coeid 23994. (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 23994*	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 23995*	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 23996*	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 23997*	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 23998*	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 23999*	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 24000*	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 )