P. 265 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26401-26500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fta1glem2 26401*	Lemma for fta1g 26402. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑊 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}))    &   ⊢ (𝜑 → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑁 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))    ⇒   ⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹))
Theorem	fta1g 26402	The one-sided fundamental theorem of algebra. A polynomial of degree 𝑛 has at most 𝑛 roots. Unlike the real fundamental theorem fta 27324, 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 26403	Lemma for fta1b 26404. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑊 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐾)    &   ⊢ (𝜑 → (𝑀 × 𝑁) = 𝑊)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑊)    &   ⊢ (𝜑 → ((𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 }) → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ (𝐷‘(𝑀 · 𝑋))))    ⇒   ⊢ (𝜑 → 𝑁 = 𝑊)
Theorem	fta1b 26404*	The assumption that 𝑅 be a domain in fta1g 26402 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 26405*	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 26406	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 26407*	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 26408*	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 26409	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 26410	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 26411	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 26412	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 26413	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 26414	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 26415	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 26416	Extend class notation to include the set of complex polynomials.
class Poly
Syntax	cidp 26417	Extend class notation to include the identity polynomial.
class Xp
Syntax	ccoe 26418	Extend class notation to include the coefficient function on polynomials.
class coeff
Syntax	cdgr 26419	Extend class notation to include the degree function on polynomials.
class deg
Definition	df-ply 26420*	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 26421	Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ Xp = ( I ↾ ℂ)
Definition	df-coe 26422*	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 26423	Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup((◡(coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
Theorem	plyco0 26424*	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 26425*	Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝑆 ⊆ ℂ → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
Theorem	plybss 26426	Reverse closure of the parameter 𝑆 of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ)
Theorem	elply 26427*	Definition of a polynomial with coefficients in 𝑆. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
Theorem	elply2 26428*	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 26429	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 26430	A polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
Theorem	plyss 26431	The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇))
Theorem	plyssc 26432	Every polynomial ring is contained in the ring of polynomials over ℂ. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (Poly‘𝑆) ⊆ (Poly‘ℂ)
Theorem	elplyr 26433*	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 26434*	Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
Theorem	ply1termlem 26435*	Lemma for ply1term 26436. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))))
Theorem	ply1term 26436*	A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆))
Theorem	plypow 26437*	A power is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑁)) ∈ (Poly‘𝑆))
Theorem	plyconst 26438	A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆) → (ℂ × {𝐴}) ∈ (Poly‘𝑆))
Theorem	ne0p 26439	A test to show that a polynomial is nonzero. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐹‘𝐴) ≠ 0) → 𝐹 ≠ 0𝑝)
Theorem	ply0 26440	The zero function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝑆 ⊆ ℂ → 0𝑝 ∈ (Poly‘𝑆))
Theorem	plyid 26441	The identity function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆) → Xp ∈ (Poly‘𝑆))
Theorem	idpfv 26442	Value of the identity polynomial. (Contributed by SN, 30-Aug-2026.)
⊢ (𝐴 ∈ ℂ → (Xp‘𝐴) = 𝐴)
Theorem	plyeq0lem 26443*	Lemma for plyeq0 26444. 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 26444*	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 26422 is well-defined. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → 𝐴 = (ℕ0 × {0}))
Theorem	plypf1 26445	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 26446*	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 26447*	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 26448*	Lemma for plyadd 26450. (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 26449*	Lemma for plymul 26451. (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 26450*	The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ (Poly‘𝑆))
Theorem	plymul 26451*	The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ (Poly‘𝑆))
Theorem	plysub 26452*	The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ (Poly‘𝑆))
Theorem	plyaddcl 26453	The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f + 𝐺) ∈ (Poly‘ℂ))
Theorem	plymulcl 26454	The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f · 𝐺) ∈ (Poly‘ℂ))
Theorem	plysubcl 26455	The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f − 𝐺) ∈ (Poly‘ℂ))
Theorem	coeval 26456*	Value of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹) = (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))
Theorem	coeeulem 26457*	Lemma for coeeu 26458. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ↑m ℕ0))    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ↑m ℕ0))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	coeeu 26458*	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 26459*	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 26460*	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 26461	Value of the degree function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) = sup((◡𝐴 “ (ℂ ∖ {0})), ℕ0, < ))
Theorem	dgrlem 26462*	Lemma for dgrcl 26466 and similar theorems. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛))
Theorem	coef 26463	The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶(𝑆 ∪ {0}))
Theorem	coef2 26464	The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → 𝐴:ℕ0⟶𝑆)
Theorem	coef3 26465	The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
Theorem	dgrcl 26466	The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈ ℕ0)
Theorem	dgrub 26467	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 26468	All the coefficients above the degree of 𝐹 are zero. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})
Theorem	dgrlb 26469	If all the coefficients above 𝑀 are zero, then the degree of 𝐹 is at most 𝑀. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0}) → 𝑁 ≤ 𝑀)
Theorem	coeidlem 26470*	Lemma for coeid 26471. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐵‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))
Theorem	coeid 26471*	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.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))
Theorem	coeid2 26472*	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.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑋 ∈ ℂ) → (𝐹‘𝑋) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑋↑𝑘)))
Theorem	coeid3 26473*	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.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑋 ∈ ℂ) → (𝐹‘𝑋) = Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑋↑𝑘)))
Theorem	plyco 26474*	The composition of two polynomials is a polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (Poly‘𝑆))
Theorem	coeeq2 26475*	Compute the coefficient function given a sum expression for the polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0)))
Theorem	dgrle 26476*	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.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → (deg‘𝐹) ≤ 𝑁)
Theorem	dgreq 26477*	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.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → (𝐴‘𝑁) ≠ 0)    ⇒   ⊢ (𝜑 → (deg‘𝐹) = 𝑁)
Theorem	0dgr 26478	A constant function has degree 0. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (deg‘(ℂ × {𝐴})) = 0)
Theorem	0dgrb 26479	A function has degree zero iff it is a constant function. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)})))
Theorem	dgrnznn 26480	A nonzero polynomial with a root has positive degree. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (((𝑃 ∈ (Poly‘𝑆) ∧ 𝑃 ≠ 0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (deg‘𝑃) ∈ ℕ)
Theorem	coefv0 26481	The result of evaluating a polynomial at zero is the constant term. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0))
Theorem	coeaddlem 26482	Lemma for coeadd 26484 and dgradd 26500. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    &   ⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐹 ∘f + 𝐺)) = (𝐴 ∘f + 𝐵) ∧ (deg‘(𝐹 ∘f + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)))
Theorem	coemullem 26483*	Lemma for coemul 26485 and dgrmul 26503. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    &   ⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐹 ∘f · 𝐺)) = (𝑛 ∈ ℕ0 ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘)))) ∧ (deg‘(𝐹 ∘f · 𝐺)) ≤ (𝑀 + 𝑁)))
Theorem	coeadd 26484	The coefficient function of a sum is the sum of coefficients. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘f + 𝐺)) = (𝐴 ∘f + 𝐵))
Theorem	coemul 26485*	A coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0) → ((coeff‘(𝐹 ∘f · 𝐺))‘𝑁) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝐵‘(𝑁 − 𝑘))))
Theorem	coe11 26486	The coefficient function is one-to-one, so if the coefficients are equal then the functions are equal and vice-versa. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 = 𝐺 ↔ 𝐴 = 𝐵))
Theorem	coemulhi 26487	The leading coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    &   ⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐹 ∘f · 𝐺))‘(𝑀 + 𝑁)) = ((𝐴‘𝑀) · (𝐵‘𝑁)))
Theorem	coemulc 26488	The coefficient function is linear under scalar multiplication. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘((ℂ × {𝐴}) ∘f · 𝐹)) = ((ℕ0 × {𝐴}) ∘f · (coeff‘𝐹)))
Theorem	coe0 26489	The coefficients of the zero polynomial are zero. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (coeff‘0𝑝) = (ℕ0 × {0})
Theorem	coesub 26490	The coefficient function of a sum is the sum of coefficients. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘f − 𝐺)) = (𝐴 ∘f − 𝐵))
Theorem	coe1termlem 26491*	The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((coeff‘𝐹) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) ∧ (𝐴 ≠ 0 → (deg‘𝐹) = 𝑁)))
Theorem	coe1term 26492*	The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((coeff‘𝐹)‘𝑀) = if(𝑀 = 𝑁, 𝐴, 0))
Theorem	dgr1term 26493*	The degree of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℕ0) → (deg‘𝐹) = 𝑁)
Theorem	plycn 26494	A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 11208. (Revised by GG, 16-Mar-2025.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	dgr0 26495	The degree of the zero polynomial is zero. Note: this differs from some other definitions of the degree of the zero polynomial, such as -1, -∞ or undefined. But it is convenient for us to define it this way, so that we have dgrcl 26466, dgreq0 26498 and coeid 26471 without having to special-case zero, although plydivalg 26536 is a little more complicated as a result. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (deg‘0𝑝) = 0
Theorem	coeidp 26496	The coefficients of the identity function. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ (𝐴 ∈ ℕ0 → ((coeff‘Xp)‘𝐴) = if(𝐴 = 1, 1, 0))
Theorem	dgrid 26497	The degree of the identity function. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ (deg‘Xp) = 1
Theorem	dgreq0 26498	The leading coefficient of a polynomial is nonzero, unless the entire polynomial is zero. (Contributed by Mario Carneiro, 22-Jul-2014.) (Proof shortened by Fan Zheng, 21-Jun-2016.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
Theorem	dgrlt 26499	Two ways to say that the degree of 𝐹 is strictly less than 𝑁. (Contributed by Mario Carneiro, 25-Jul-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0) → ((𝐹 = 0𝑝 ∨ 𝑁 < 𝑀) ↔ (𝑁 ≤ 𝑀 ∧ (𝐴‘𝑀) = 0)))
Theorem	dgradd 26500	The degree of a sum of polynomials is at most the maximum of the degrees. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘f + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))