P. 227 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22601-22700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mdegvscale 22601	The degree of a scalar multiple of a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = ( I mPoly R )   &    |- D = ( I mDeg R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- K = ( Base ` R )   &    |- .x. = ( .s ` Y )   &    |- ( ph -> F e. K )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( D ` ( F .x. G ) ) <_ ( D ` G ) )
Theorem	mdegvsca 22602	The degree of a scalar multiple of a polynomial is exactly the degree of the original polynomial when the multiple is a non-zero-divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.)
|- Y = ( I mPoly R )   &    |- D = ( I mDeg R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- E = (RLReg ` R )   &    |- .x. = ( .s ` Y )   &    |- ( ph -> F e. E )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( D ` ( F .x. G ) ) = ( D ` G ) )
Theorem	mdegle0 22603	A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- Y = ( I mPoly R )   &    |- D = ( I mDeg R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- A = (algSc ` Y )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( ( D ` F ) <_ 0 <-> F = ( A ` ( F ` ( I X. { 0 } ) ) ) ) )
Theorem	mdegmullem 22604*	Lemma for mdegmulle2 22605. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = ( I mPoly R )   &    |- D = ( I mDeg R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .x. = ( .r ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> J e. NN0 )   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> ( D ` F ) <_ J )   &    |- ( ph -> ( D ` G ) <_ K )   &    |- A = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }   &    |- H = ( b e. A |-> (ℂfld gsumg b ) )   =>    |- ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )
Theorem	mdegmulle2 22605	The multivariate degree of a product of polynomials is at most the sum of the degrees of the polynomials. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = ( I mPoly R )   &    |- D = ( I mDeg R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .x. = ( .r ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> J e. NN0 )   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> ( D ` F ) <_ J )   &    |- ( ph -> ( D ` G ) <_ K )   =>    |- ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )
Theorem	deg1fval 22606	Relate univariate polynomial degree to multivariate. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.)
|- D = ( deg1 ` R )   =>    |- D = ( 1o mDeg R )
Theorem	deg1xrf 22607	Functionality of univariate polynomial degree, weak range. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   =>    |- D : B --> RR*
Theorem	deg1xrcl 22608	Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   =>    |- ( F e. B -> ( D ` F ) e. RR* )
Theorem	deg1cl 22609	Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   =>    |- ( F e. B -> ( D ` F ) e. ( NN0 u. { -oo } ) )
Theorem	mdegpropd 22610*	Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> B = ( Base ` S ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )   =>    |- ( ph -> ( I mDeg R ) = ( I mDeg S ) )
Theorem	deg1fvi 22611	Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- ( deg1 ` R ) = ( deg1 ` ( _I ` R ) )
Theorem	deg1propd 22612*	Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> B = ( Base ` S ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )   =>    |- ( ph -> ( deg1 ` R ) = ( deg1 ` S ) )
Theorem	deg1z 22613	Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   =>    |- ( R e. Ring -> ( D ` .0. ) = -oo )
Theorem	deg1nn0cl 22614	Degree of a nonzero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   =>    |- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
Theorem	deg1n0ima 22615	Degree image of a set of polynomials which does not include zero. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   =>    |- ( R e. Ring -> ( D " ( B \ { .0. } ) ) C_ NN0 )
Theorem	deg1nn0clb 22616	A polynomial is nonzero iff it has definite degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   =>    |- ( ( R e. Ring /\ F e. B ) -> ( F =/= .0. <-> ( D ` F ) e. NN0 ) )
Theorem	deg1lt0 22617	A polynomial is zero iff it has negative degree. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   =>    |- ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) < 0 <-> F = .0. ) )
Theorem	deg1ldg 22618	A nonzero univariate polynomial always has a nonzero leading coefficient. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   &    |- Y = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) =/= Y )
Theorem	deg1ldgn 22619	An index at which a polynomial is zero, cannot be its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   &    |- Y = ( 0g ` R )   &    |- A = (coe1 ` F )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> X e. NN0 )   &    |- ( ph -> ( A ` X ) = Y )   =>    |- ( ph -> ( D ` F ) =/= X )
Theorem	deg1ldgdomn 22620	A nonzero univariate polynomial over a domain always has a non-zero-divisor leading coefficient. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- B = ( Base ` P )   &    |- E = (RLReg ` R )   &    |- A = (coe1 ` F )   =>    |- ( ( R e. Domn /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) e. E )
Theorem	deg1leb 22621*	Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( ( F e. B /\ G e. RR* ) -> ( ( D ` F ) <_ G <-> A. x e. NN0 ( G < x -> ( A ` x ) = .0. ) ) )
Theorem	deg1val 22622	Value of the univariate degree as a supremum. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Jul-2019.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( F e. B -> ( D ` F ) = sup ( ( A supp .0. ) , RR* , < ) )
Theorem	deg1valOLD 22623	Value of the univariate degree as a supremum. (Contributed by Stefan O'Rear, 29-Mar-2015.) Obsolete version of deg1val 22622 as of 25-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( F e. B -> ( D ` F ) = sup ( ( `' A " ( _V \ { .0. } ) ) , RR* , < ) )
Theorem	deg1lt 22624	If the degree of a univariate polynomial is less than some index, then that coefficient must be zero. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( A ` G ) = .0. )
Theorem	deg1ge 22625	Conversely, a nonzero coefficient sets a lower bound on the degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` R )   &    |- A = (coe1 ` F )   =>    |- ( ( F e. B /\ G e. NN0 /\ ( A ` G ) =/= .0. ) -> G <_ ( D ` F ) )
Theorem	coe1mul3 22626	The coefficient vector of multiplication in the univariate polynomial ring, at indices high enough that at most one component can be active in the sum. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- .xb = ( .r ` Y )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` Y )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> I e. NN0 )   &    |- ( ph -> ( D ` F ) <_ I )   &    |- ( ph -> G e. B )   &    |- ( ph -> J e. NN0 )   &    |- ( ph -> ( D ` G ) <_ J )   =>    |- ( ph -> ( (coe1 ` ( F .xb G ) ) ` ( I + J ) ) = ( ( (coe1 ` F ) ` I ) .x. ( (coe1 ` G ) ` J ) ) )
Theorem	coe1mul4 22627	Value of the "leading" coefficient of a product of two nonzero polynomials. This will fail to actually be the leading coefficient only if it is zero (requiring the basic ring to contain zero divisors). (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- .xb = ( .r ` Y )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` Y )   &    |- D = ( deg1 ` R )   &    |- .0. = ( 0g ` Y )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> F =/= .0. )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   =>    |- ( ph -> ( (coe1 ` ( F .xb G ) ) ` ( ( D ` F ) + ( D ` G ) ) ) = ( ( (coe1 ` F ) ` ( D ` F ) ) .x. ( (coe1 ` G ) ` ( D ` G ) ) ) )
Theorem	deg1addle 22628	The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
Theorem	deg1addle2 22629	If both factors have degree bounded by L, then the sum of the polynomials also has degree bounded by L. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> L e. RR* )   &    |- ( ph -> ( D ` F ) <_ L )   &    |- ( ph -> ( D ` G ) <_ L )   =>    |- ( ph -> ( D ` ( F .+ G ) ) <_ L )
Theorem	deg1add 22630	Exact degree of a sum of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> ( D ` G ) < ( D ` F ) )   =>    |- ( ph -> ( D ` ( F .+ G ) ) = ( D ` F ) )
Theorem	deg1vscale 22631	The degree of a scalar times a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- K = ( Base ` R )   &    |- .x. = ( .s ` Y )   &    |- ( ph -> F e. K )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( D ` ( F .x. G ) ) <_ ( D ` G ) )
Theorem	deg1vsca 22632	The degree of a scalar times a polynomial is exactly the degree of the original polynomial when the scalar is not a zero divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- E = (RLReg ` R )   &    |- .x. = ( .s ` Y )   &    |- ( ph -> F e. E )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( D ` ( F .x. G ) ) = ( D ` G ) )
Theorem	deg1invg 22633	The degree of the negated polynomial is the same as the original. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- N = ( invg ` Y )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( D ` ( N ` F ) ) = ( D ` F ) )
Theorem	deg1suble 22634	The degree of a difference of polynomials is bounded by the maximum of degrees. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .- = ( -g ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( D ` ( F .- G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
Theorem	deg1sub 22635	Exact degree of a difference of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .- = ( -g ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> ( D ` G ) < ( D ` F ) )   =>    |- ( ph -> ( D ` ( F .- G ) ) = ( D ` F ) )
Theorem	deg1mulle2 22636	Produce a bound on the product of two univariate polynomials given bounds on the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- ( ph -> R e. Ring )   &    |- B = ( Base ` Y )   &    |- .x. = ( .r ` Y )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> J e. NN0 )   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> ( D ` F ) <_ J )   &    |- ( ph -> ( D ` G ) <_ K )   =>    |- ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )
Theorem	deg1sublt 22637	Subtraction of two polynomials limited to the same degree with the same leading coefficient gives a polynomial with a smaller degree. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .- = ( -g ` P )   &    |- ( ph -> L e. NN0 )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> ( D ` F ) <_ L )   &    |- ( ph -> G e. B )   &    |- ( ph -> ( D ` G ) <_ L )   &    |- A = (coe1 ` F )   &    |- C = (coe1 ` G )   &    |- ( ph -> ( (coe1 ` F ) ` L ) = ( (coe1 ` G ) ` L ) )   =>    |- ( ph -> ( D ` ( F .- G ) ) < L )
Theorem	deg1le0 22638	A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) <_ 0 <-> F = ( A ` ( (coe1 ` F ) ` 0 ) ) ) )
Theorem	deg1sclle 22639	A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ F e. K ) -> ( D ` ( A ` F ) ) <_ 0 )
Theorem	deg1scl 22640	A nonzero scalar polynomial has zero degree. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ F e. K /\ F =/= .0. ) -> ( D ` ( A ` F ) ) = 0 )
Theorem	deg1mul2 22641	Degree of multiplication of two nonzero polynomials when the first leads with a non-zero-divisor coefficient. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- E = (RLReg ` R )   &    |- B = ( Base ` P )   &    |- .x. = ( .r ` P )   &    |- .0. = ( 0g ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> F =/= .0. )   &    |- ( ph -> ( (coe1 ` F ) ` ( D ` F ) ) e. E )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   =>    |- ( ph -> ( D ` ( F .x. G ) ) = ( ( D ` F ) + ( D ` G ) ) )
Theorem	deg1mul3 22642	Degree of multiplication of a polynomial on the left by a non-zero-dividing scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Jul-2019.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- E = (RLReg ` R )   &    |- B = ( Base ` P )   &    |- .x. = ( .r ` P )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( D ` ( ( A ` F ) .x. G ) ) = ( D ` G ) )
Theorem	deg1mul3le 22643	Degree of multiplication of a polynomial on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- K = ( Base ` R )   &    |- B = ( Base ` P )   &    |- .x. = ( .r ` P )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( D ` ( ( A ` F ) .x. G ) ) <_ ( D ` G ) )
Theorem	deg1tmle 22644	Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- D = ( deg1 ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( ( R e. Ring /\ C e. K /\ F e. NN0 ) -> ( D ` ( C .x. ( F .^ X ) ) ) <_ F )
Theorem	deg1tm 22645	Exact degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- D = ( deg1 ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> ( D ` ( C .x. ( F .^ X ) ) ) = F )
Theorem	deg1pwle 22646	Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( ( R e. Ring /\ F e. NN0 ) -> ( D ` ( F .^ X ) ) <_ F )
Theorem	deg1pw 22647	Exact degree of a variable power over a nontrivial ring. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- D = ( deg1 ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( ( R e. NzRing /\ F e. NN0 ) -> ( D ` ( F .^ X ) ) = F )
Theorem	ply1nz 22648	Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. NzRing -> P e. NzRing )
Theorem	ply1nzb 22649	Univariate polynomials are nonzero iff the base is nonzero. Or in contraposition, the univariate polynomials over the zero ring are also zero. (Contributed by Mario Carneiro, 13-Jun-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. Ring -> ( R e. NzRing <-> P e. NzRing ) )
Theorem	ply1domn 22650	Corollary of deg1mul2 22641: the univariate polynomials over a domain are a domain. This is true for multivariate but with a much more complicated proof. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. Domn -> P e. Domn )
Theorem	ply1idom 22651	The ring of univariate polynomials over an integral domain is itself an integral domain. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. IDomn -> P e. IDomn )
14.1.2  The division algorithm for univariate polynomials
Syntax	cmn1 22652	Monic polynomials.
class Monic1p
Syntax	cuc1p 22653	Unitic polynomials.
class Unic1p
Syntax	cq1p 22654	Univariate polynomial quotient.
class quot1p
Syntax	cr1p 22655	Univariate polynomial remainder.
class rem1p
Syntax	cig1p 22656	Univariate polynomial ideal generator.
class idlGen1p
Definition	df-mon1 22657*	Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Monic1p = ( r e. _V |-> { f e. ( Base ` (Poly1 ` r ) ) | ( f =/= ( 0g ` (Poly1 ` r ) ) /\ ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } )
Definition	df-uc1p 22658*	Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg 22664. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- Unic1p = ( r e. _V |-> { f e. ( Base ` (Poly1 ` r ) ) | ( f =/= ( 0g ` (Poly1 ` r ) ) /\ ( (coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. (Unit ` r ) ) } )
Definition	df-q1p 22659*	Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 22664. We actually use the reversed version for better harmony with our divisibility df-dvdsr 17417. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- quot1p = ( r e. _V |-> [_ (Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )
Definition	df-r1p 22660*	Define the remainder after dividing two univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- rem1p = ( r e. _V |-> [_ ( Base ` (Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` (Poly1 ` r ) ) ( ( f (quot1p ` r ) g ) ( .r ` (Poly1 ` r ) ) g ) ) ) )
Definition	df-ig1p 22661*	Define a choice function for generators of ideals over a division ring; this is the unique monic polynomial of minimal degree in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- idlGen1p = ( r e. _V |-> ( i e. (LIdeal ` (Poly1 ` r ) ) |-> if ( i = { ( 0g ` (Poly1 ` r ) ) } , ( 0g ` (Poly1 ` r ) ) , ( iota_ g e. ( i i^i (Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = sup ( ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) ) , RR , `' < ) ) ) ) )
Theorem	ply1divmo 22662*	Uniqueness of a quotient in a polynomial division. For polynomials F , G such that G =/= 0 and the leading coefficient of G is not a zero divisor, there is at most one polynomial q which satisfies F = ( G x. q ) + r where the degree of r is less than the degree of G. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by NM, 17-Jun-2017.)
|- P = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- .- = ( -g ` P )   &    |- .0. = ( 0g ` P )   &    |- .xb = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   &    |- ( ph -> ( (coe1 ` G ) ` ( D ` G ) ) e. E )   &    |- E = (RLReg ` R )   =>    |- ( ph -> E* q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )
Theorem	ply1divex 22663*	Lemma for ply1divalg 22664: existence part. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- P = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- .- = ( -g ` P )   &    |- .0. = ( 0g ` P )   &    |- .xb = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   &    |- .1. = ( 1r ` R )   &    |- K = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> I e. K )   &    |- ( ph -> ( ( (coe1 ` G ) ` ( D ` G ) ) .x. I ) = .1. )   =>    |- ( ph -> E. q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )
Theorem	ply1divalg 22664*	The division algorithm for univariate polynomials over a ring. For polynomials F , G such that G =/= 0 and the leading coefficient of G is a unit, there are unique polynomials q and r = F - ( G x. q ) such that the degree of r is less than the degree of G. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- P = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- .- = ( -g ` P )   &    |- .0. = ( 0g ` P )   &    |- .xb = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   &    |- ( ph -> ( (coe1 ` G ) ` ( D ` G ) ) e. U )   &    |- U = (Unit ` R )   =>    |- ( ph -> E! q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )
Theorem	ply1divalg2 22665*	Reverse the order of multiplication in ply1divalg 22664 via the opposite ring. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- .- = ( -g ` P )   &    |- .0. = ( 0g ` P )   &    |- .xb = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> G =/= .0. )   &    |- ( ph -> ( (coe1 ` G ) ` ( D ` G ) ) e. U )   &    |- U = (Unit ` R )   =>    |- ( ph -> E! q e. B ( D ` ( F .- ( q .xb G ) ) ) < ( D ` G ) )
Theorem	uc1pval 22666*	Value of the set of unitic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` P )   &    |- D = ( deg1 ` R )   &    |- C = (Unic1p ` R )   &    |- U = (Unit ` R )   =>    |- C = { f e. B | ( f =/= .0. /\ ( (coe1 ` f ) ` ( D ` f ) ) e. U ) }
Theorem	isuc1p 22667	Being a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- .0. = ( 0g ` P )   &    |- D = ( deg1 ` R )   &    |- C = (Unic1p ` R )   &    |- U = (Unit ` R )   =>    |- ( F e. C <-> ( F e. B /\ F =/= .0. /\ ( (coe1 ` F ) ` ( D ` F ) ) e. U ) )
Theorem	mon1pval 22668*	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 22669	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 22670	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 22671	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 22672	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 22673	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 22674	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 22675	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 22676	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 22677	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 22678	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 22679	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 22680*	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 22681	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 22682	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 22683	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 22684	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 22685	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 22686	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 22687	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 22688	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 22689	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 22690	The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 14192). 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 22691	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 22692	Lemma for fta1g 22694. (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 22693*	Lemma for fta1g 22694. (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 22694	The one-sided fundamental theorem of algebra. A polynomial of degree n has at most n roots. Unlike the real fundamental theorem fta 23479, 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 22695	Lemma for fta1b 22696. (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 22696*	The assumption that R be a domain in fta1g 22694 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 22697	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 22698*	There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- 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 ) = sup ( ( D " ( I \ { .0. } ) ) , RR , `' < ) )
Theorem	ig1pval 22699*	Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- 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 ) = sup ( ( D " ( I \ { .0. } ) ) , RR , `' < ) ) ) )
Theorem	ig1pval2 22700	Generator of the zero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- G = (idlGen1p ` R )   &    |- .0. = ( 0g ` P )   =>    |- ( R e. Ring -> ( G ` { .0. } ) = .0. )