P. 262 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26101-26200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ply1divmo 26101*	Uniqueness of a quotient in a polynomial division. For polynomials 𝐹, 𝐺 such that 𝐺 ≠ 0 and the leading coefficient of 𝐺 is not a zero divisor, there is at most one polynomial 𝑞 which satisfies 𝐹 = (𝐺 · 𝑞) + 𝑟 where the degree of 𝑟 is less than the degree of 𝐺. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by NM, 17-Jun-2017.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ≠ 0 )    &   ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝐸)    &   ⊢ 𝐸 = (RLReg‘𝑅)    ⇒   ⊢ (𝜑 → ∃*𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))
Theorem	ply1divex 26102*	Lemma for ply1divalg 26103: existence part. (Contributed by Stefan O'Rear, 27-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ≠ 0 )    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐾)    &   ⊢ (𝜑 → (((coe1‘𝐺)‘(𝐷‘𝐺)) · 𝐼) = 1 )    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))
Theorem	ply1divalg 26103*	The division algorithm for univariate polynomials over a ring. For polynomials 𝐹, 𝐺 such that 𝐺 ≠ 0 and the leading coefficient of 𝐺 is a unit, there are unique polynomials 𝑞 and 𝑟 = 𝐹 − (𝐺 · 𝑞) such that the degree of 𝑟 is less than the degree of 𝐺. (Contributed by Stefan O'Rear, 27-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ≠ 0 )    &   ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝑈)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))
Theorem	ply1divalg2 26104*	Reverse the order of multiplication in ply1divalg 26103 via the opposite ring. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ≠ 0 )    &   ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝑈)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 ∙ 𝐺))) < (𝐷‘𝐺))
Theorem	uc1pval 26105*	Value of the set of unitic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ 𝐶 = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧ ((coe1‘𝑓)‘(𝐷‘𝑓)) ∈ 𝑈)}
Theorem	isuc1p 26106	Being a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐶 ↔ (𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝑈))
Theorem	mon1pval 26107*	Value of the set of monic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ 𝑀 = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧ ((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )}
Theorem	ismon1p 26108	Being a monic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝑀 ↔ (𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1 ))
Theorem	uc1pcl 26109	Unitic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐶 → 𝐹 ∈ 𝐵)
Theorem	mon1pcl 26110	Monic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝑀 → 𝐹 ∈ 𝐵)
Theorem	uc1pn0 26111	Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐶 → 𝐹 ≠ 0 )
Theorem	mon1pn0 26112	Monic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝑀 → 𝐹 ≠ 0 )
Theorem	uc1pdeg 26113	Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶) → (𝐷‘𝐹) ∈ ℕ0)
Theorem	uc1pldg 26114	Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐶 → ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝑈)
Theorem	mon1pldg 26115	Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝑀 → ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1 )
Theorem	mon1puc1p 26116	Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀) → 𝑋 ∈ 𝐶)
Theorem	uc1pmon1p 26117	Make a unitic polynomial monic by multiplying a factor to normalize the leading coefficient. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ · = (.r‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶) → ((𝐴‘(𝐼‘((coe1‘𝑋)‘(𝐷‘𝑋)))) · 𝑋) ∈ 𝑀)
Theorem	deg1submon1p 26118	The difference of two monic polynomials of the same degree is a polynomial of lesser degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑂 = (Monic1p‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑂)    &   ⊢ (𝜑 → (𝐷‘𝐹) = 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑂)    &   ⊢ (𝜑 → (𝐷‘𝐺) = 𝑋)    ⇒   ⊢ (𝜑 → (𝐷‘(𝐹 − 𝐺)) < 𝑋)
Theorem	mon1pid 26119	Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 1 = (1r‘𝑃)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing → ( 1 ∈ 𝑀 ∧ (𝐷‘ 1 ) = 0))
Theorem	q1pval 26120*	Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑄 = (quot1p‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ · = (.r‘𝑃)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝑄𝐺) = (℩𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺)))
Theorem	q1peqb 26121	Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑄 = (quot1p‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((𝑋 ∈ 𝐵 ∧ (𝐷‘(𝐹 − (𝑋 · 𝐺))) < (𝐷‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑋))
Theorem	q1pcl 26122	Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑄 = (quot1p‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝑄𝐺) ∈ 𝐵)
Theorem	r1pval 26123	Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑄 = (quot1p‘𝑅)    &   ⊢ · = (.r‘𝑃)    &   ⊢ − = (-g‘𝑃)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝐸𝐺) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺)))
Theorem	r1pcl 26124	Closure of remainder following division by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝐸𝐺) ∈ 𝐵)
Theorem	r1pdeglt 26125	The remainder has a degree less than the divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐷‘(𝐹𝐸𝐺)) < (𝐷‘𝐺))
Theorem	r1pid 26126	Express the original polynomial 𝐹 as 𝐹 = (𝑞 · 𝐺) + 𝑟 using the quotient and remainder functions for 𝑞 and 𝑟. (Contributed by Mario Carneiro, 5-Jun-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ 𝑄 = (quot1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ · = (.r‘𝑃)    &   ⊢ + = (+g‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → 𝐹 = (((𝐹𝑄𝐺) · 𝐺) + (𝐹𝐸𝐺)))
Theorem	r1pid2 26127	Identity law for polynomial remainder operation: it leaves a polynomial 𝐴 unchanged iff the degree of 𝐴 is less than the degree of the divisor 𝐵. (Contributed by Thierry Arnoux, 2-Apr-2025.) Generalize to domains. (Revised by SN, 21-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ (𝐷‘𝐴) < (𝐷‘𝐵)))
Theorem	dvdsq1p 26128	Divisibility in a polynomial ring is witnessed by the quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ ∥ = (∥r‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ · = (.r‘𝑃)    &   ⊢ 𝑄 = (quot1p‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ 𝐹 = ((𝐹𝑄𝐺) · 𝐺)))
Theorem	dvdsr1p 26129	Divisibility in a polynomial ring in terms of the remainder. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ ∥ = (∥r‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐸 = (rem1p‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ (𝐹𝐸𝐺) = 0 ))
Theorem	ply1remlem 26130	A term of the form 𝑥 − 𝑁 is linear, monic, and has exactly one zero. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘𝑁))    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐾)    &   ⊢ 𝑈 = (Monic1p‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝑈 ∧ (𝐷‘𝐺) = 1 ∧ (◡(𝑂‘𝐺) “ { 0 }) = {𝑁}))
Theorem	ply1rem 26131	The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 16512). If a polynomial 𝐹 is divided by the linear factor 𝑥 − 𝐴, the remainder is equal to 𝐹(𝐴), the evaluation of the polynomial at 𝐴 (interpreted as a constant polynomial). (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘𝑁))    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝐸 = (rem1p‘𝑅)    ⇒   ⊢ (𝜑 → (𝐹𝐸𝐺) = (𝐴‘((𝑂‘𝐹)‘𝑁)))
Theorem	facth1 26132	The factor theorem and its converse. A polynomial 𝐹 has a root at 𝐴 iff 𝐺 = 𝑥 − 𝐴 is a factor of 𝐹. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘𝑁))    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ ∥ = (∥r‘𝑃)    ⇒   ⊢ (𝜑 → (𝐺 ∥ 𝐹 ↔ ((𝑂‘𝐹)‘𝑁) = 0 ))
Theorem	fta1glem1 26133	Lemma for fta1g 26135. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑊 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}))    ⇒   ⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁)
Theorem	fta1glem2 26134*	Lemma for fta1g 26135. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑊 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}))    &   ⊢ (𝜑 → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑁 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))    ⇒   ⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹))
Theorem	fta1g 26135	The one-sided fundamental theorem of algebra. A polynomial of degree 𝑛 has at most 𝑛 roots. Unlike the real fundamental theorem fta 27043, which is only true in ℂ and other algebraically closed fields, this is true in any integral domain. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑊 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ≠ 0 )    ⇒   ⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹))
Theorem	fta1blem 26136	Lemma for fta1b 26137. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑊 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐾)    &   ⊢ (𝜑 → (𝑀 × 𝑁) = 𝑊)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑊)    &   ⊢ (𝜑 → ((𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 }) → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ (𝐷‘(𝑀 · 𝑋))))    ⇒   ⊢ (𝜑 → 𝑁 = 𝑊)
Theorem	fta1b 26137*	The assumption that 𝑅 be a domain in fta1g 26135 is necessary. Here we show that the statement is strong enough to prove that 𝑅 is a domain. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑊 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    ⇒   ⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀𝑓 ∈ (𝐵 ∖ { 0 })(♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))
Theorem	idomrootle 26138*	No element of an integral domain can have more than 𝑁 𝑁-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    ⇒   ⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (♯‘{𝑦 ∈ 𝐵 ∣ (𝑁 ↑ 𝑦) = 𝑋}) ≤ 𝑁)
Theorem	drnguc1p 26139	Over a division ring, all nonzero polynomials are unitic. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → 𝐹 ∈ 𝐶)
Theorem	ig1peu 26140*	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.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃!𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
Theorem	ig1pval 26141*	Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈) → (𝐺‘𝐼) = if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))))
Theorem	ig1pval2 26142	Generator of the zero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐺‘{ 0 }) = 0 )
Theorem	ig1pval3 26143	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.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ((𝐺‘𝐼) ∈ 𝐼 ∧ (𝐺‘𝐼) ∈ 𝑀 ∧ (𝐷‘(𝐺‘𝐼)) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
Theorem	ig1pcl 26144	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.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈) → (𝐺‘𝐼) ∈ 𝐼)
Theorem	ig1pdvds 26145	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.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ ∥ = (∥r‘𝑃)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼) → (𝐺‘𝐼) ∥ 𝑋)
Theorem	ig1prsp 26146	Any ideal of polynomials over a division ring is generated by the ideal's canonical generator. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝐾 = (RSpan‘𝑃)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈) → 𝐼 = (𝐾‘{(𝐺‘𝐼)}))
Theorem	ply1lpir 26147	The ring of polynomials over a division ring has the principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 𝑃 ∈ LPIR)
Theorem	ply1pid 26148	The polynomials over a field are a PID. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ Field → 𝑃 ∈ PID)
14.1.3  Elementary properties of complex polynomials
Syntax	cply 26149	Extend class notation to include the set of complex polynomials.
class Poly
Syntax	cidp 26150	Extend class notation to include the identity polynomial.
class Xp
Syntax	ccoe 26151	Extend class notation to include the coefficient function on polynomials.
class coeff
Syntax	cdgr 26152	Extend class notation to include the degree function on polynomials.
class deg
Definition	df-ply 26153*	Define the set of polynomials on the complex numbers with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ Poly = (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
Definition	df-idp 26154	Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ Xp = ( I ↾ ℂ)
Definition	df-coe 26155*	Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ coeff = (𝑓 ∈ (Poly‘ℂ) ↦ (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))
Definition	df-dgr 26156	Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup((◡(coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
Theorem	plyco0 26157*	Two ways to say that a function on the nonnegative integers has finite support. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)))
Theorem	plyval 26158*	Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝑆 ⊆ ℂ → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
Theorem	plybss 26159	Reverse closure of the parameter 𝑆 of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ)
Theorem	elply 26160*	Definition of a polynomial with coefficients in 𝑆. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
Theorem	elply2 26161*	The coefficient function can be assumed to have zeroes outside 0...𝑛. (Contributed by Mario Carneiro, 20-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))
Theorem	plyun0 26162	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‘(𝑆 ∪ {0})) = (Poly‘𝑆)
Theorem	plyf 26163	A polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
Theorem	plyss 26164	The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇))
Theorem	plyssc 26165	Every polynomial ring is contained in the ring of polynomials over ℂ. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (Poly‘𝑆) ⊆ (Poly‘ℂ)
Theorem	elplyr 26166*	Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
Theorem	elplyd 26167*	Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
Theorem	ply1termlem 26168*	Lemma for ply1term 26169. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))))
Theorem	ply1term 26169*	A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆))
Theorem	plypow 26170*	A power is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑁)) ∈ (Poly‘𝑆))
Theorem	plyconst 26171	A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆) → (ℂ × {𝐴}) ∈ (Poly‘𝑆))
Theorem	ne0p 26172	A test to show that a polynomial is nonzero. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐹‘𝐴) ≠ 0) → 𝐹 ≠ 0𝑝)
Theorem	ply0 26173	The zero function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝑆 ⊆ ℂ → 0𝑝 ∈ (Poly‘𝑆))
Theorem	plyid 26174	The identity function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆) → Xp ∈ (Poly‘𝑆))
Theorem	plyeq0lem 26175*	Lemma for plyeq0 26176. If 𝐴 is the coefficient function for a nonzero polynomial such that 𝑃(𝑧) = Σ𝑘 ∈ ℕ0𝐴(𝑘) · 𝑧↑𝑘 = 0 for every 𝑧 ∈ ℂ and 𝐴(𝑀) is the nonzero leading coefficient, then the function 𝐹(𝑧) = 𝑃(𝑧) / 𝑧↑𝑀 is a sum of powers of 1 / 𝑧, and so the limit of this function as 𝑧 ⇝ +∞ is the constant term, 𝐴(𝑀). But 𝐹(𝑧) = 0 everywhere, so this limit is also equal to zero so that 𝐴(𝑀) = 0, a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ 𝑀 = sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < )    &   ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅)    ⇒   ⊢ ¬ 𝜑
Theorem	plyeq0 26176*	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 26155 is well-defined. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → 𝐴 = (ℕ0 × {0}))
Theorem	plypf1 26177	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.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝐸 = (eval1‘ℂfld)    ⇒   ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴))
Theorem	plyaddlem1 26178*	Derive the coefficient function for the sum of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → 𝐵:ℕ0⟶ℂ)    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘f + 𝐵)‘𝑘) · (𝑧↑𝑘))))
Theorem	plymullem1 26179*	Derive the coefficient function for the product of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → 𝐵:ℕ0⟶ℂ)    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛))))
Theorem	plyaddlem 26180*	Lemma for plyadd 26182. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))    &   ⊢ (𝜑 → 𝐵 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ (Poly‘𝑆))
Theorem	plymullem 26181*	Lemma for plymul 26183. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))    &   ⊢ (𝜑 → 𝐵 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ (Poly‘𝑆))
Theorem	plyadd 26182*	The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ (Poly‘𝑆))
Theorem	plymul 26183*	The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ (Poly‘𝑆))
Theorem	plysub 26184*	The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ (Poly‘𝑆))
Theorem	plyaddcl 26185	The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f + 𝐺) ∈ (Poly‘ℂ))
Theorem	plymulcl 26186	The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f · 𝐺) ∈ (Poly‘ℂ))
Theorem	plysubcl 26187	The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f − 𝐺) ∈ (Poly‘ℂ))
Theorem	coeval 26188*	Value of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹) = (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))
Theorem	coeeulem 26189*	Lemma for coeeu 26190. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ↑m ℕ0))    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ↑m ℕ0))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	coeeu 26190*	Uniqueness of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃!𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
Theorem	coelem 26191*	Lemma for properties of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → ((coeff‘𝐹) ∈ (ℂ ↑m ℕ0) ∧ ∃𝑛 ∈ ℕ0 (((coeff‘𝐹) “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘))))))
Theorem	coeeq 26192*	If 𝐴 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.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → (coeff‘𝐹) = 𝐴)
Theorem	dgrval 26193	Value of the degree function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) = sup((◡𝐴 “ (ℂ ∖ {0})), ℕ0, < ))
Theorem	dgrlem 26194*	Lemma for dgrcl 26198 and similar theorems. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛))
Theorem	coef 26195	The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶(𝑆 ∪ {0}))
Theorem	coef2 26196	The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → 𝐴:ℕ0⟶𝑆)
Theorem	coef3 26197	The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
Theorem	dgrcl 26198	The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈ ℕ0)
Theorem	dgrub 26199	If the 𝑀-th coefficient of 𝐹 is nonzero, then the degree of 𝐹 is at least 𝑀. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ≠ 0) → 𝑀 ≤ 𝑁)
Theorem	dgrub2 26200	All the coefficients above the degree of 𝐹 are zero. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})