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	ig1pdvds 26101	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 26102	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 26103	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 26104	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 26105	Extend class notation to include the set of complex polynomials.
class Poly
Syntax	cidp 26106	Extend class notation to include the identity polynomial.
class Xp
Syntax	ccoe 26107	Extend class notation to include the coefficient function on polynomials.
class coeff
Syntax	cdgr 26108	Extend class notation to include the degree function on polynomials.
class deg
Definition	df-ply 26109*	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 26110	Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ Xp = ( I ↾ ℂ)
Definition	df-coe 26111*	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 26112	Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup((◡(coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
Theorem	plyco0 26113*	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 26114*	Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝑆 ⊆ ℂ → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
Theorem	plybss 26115	Reverse closure of the parameter 𝑆 of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ)
Theorem	elply 26116*	Definition of a polynomial with coefficients in 𝑆. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
Theorem	elply2 26117*	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 26118	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 26119	A polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
Theorem	plyss 26120	The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇))
Theorem	plyssc 26121	Every polynomial ring is contained in the ring of polynomials over ℂ. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (Poly‘𝑆) ⊆ (Poly‘ℂ)
Theorem	elplyr 26122*	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 26123*	Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
Theorem	ply1termlem 26124*	Lemma for ply1term 26125. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))))
Theorem	ply1term 26125*	A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆))
Theorem	plypow 26126*	A power is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑁)) ∈ (Poly‘𝑆))
Theorem	plyconst 26127	A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆) → (ℂ × {𝐴}) ∈ (Poly‘𝑆))
Theorem	ne0p 26128	A test to show that a polynomial is nonzero. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐹‘𝐴) ≠ 0) → 𝐹 ≠ 0𝑝)
Theorem	ply0 26129	The zero function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ (𝑆 ⊆ ℂ → 0𝑝 ∈ (Poly‘𝑆))
Theorem	plyid 26130	The identity function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆) → Xp ∈ (Poly‘𝑆))
Theorem	plyeq0lem 26131*	Lemma for plyeq0 26132. 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 26132*	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 26111 is well-defined. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → 𝐴 = (ℕ0 × {0}))
Theorem	plypf1 26133	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 26134*	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 26135*	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 26136*	Lemma for plyadd 26138. (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 26137*	Lemma for plymul 26139. (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 26138*	The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ (Poly‘𝑆))
Theorem	plymul 26139*	The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ (Poly‘𝑆))
Theorem	plysub 26140*	The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ (Poly‘𝑆))
Theorem	plyaddcl 26141	The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f + 𝐺) ∈ (Poly‘ℂ))
Theorem	plymulcl 26142	The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f · 𝐺) ∈ (Poly‘ℂ))
Theorem	plysubcl 26143	The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f − 𝐺) ∈ (Poly‘ℂ))
Theorem	coeval 26144*	Value of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹) = (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))
Theorem	coeeulem 26145*	Lemma for coeeu 26146. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ↑m ℕ0))    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ↑m ℕ0))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	coeeu 26146*	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 26147*	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 26148*	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 26149	Value of the degree function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) = sup((◡𝐴 “ (ℂ ∖ {0})), ℕ0, < ))
Theorem	dgrlem 26150*	Lemma for dgrcl 26154 and similar theorems. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛))
Theorem	coef 26151	The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶(𝑆 ∪ {0}))
Theorem	coef2 26152	The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → 𝐴:ℕ0⟶𝑆)
Theorem	coef3 26153	The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
Theorem	dgrcl 26154	The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈ ℕ0)
Theorem	dgrub 26155	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 26156	All the coefficients above the degree of 𝐹 are zero. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})
Theorem	dgrlb 26157	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 26158*	Lemma for coeid 26159. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐵‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))
Theorem	coeid 26159*	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 26160*	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 26161*	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 26162*	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 26163*	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 26164*	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 26165*	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 26166	A constant function has degree 0. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (deg‘(ℂ × {𝐴})) = 0)
Theorem	0dgrb 26167	A function has degree zero iff it is a constant function. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ (𝐹 ∈ (Poly‘𝑆) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)})))
Theorem	dgrnznn 26168	A nonzero polynomial with a root has positive degree. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (((𝑃 ∈ (Poly‘𝑆) ∧ 𝑃 ≠ 0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (deg‘𝑃) ∈ ℕ)
Theorem	coefv0 26169	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 26170	Lemma for coeadd 26172 and dgradd 26189. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    &   ⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐹 ∘f + 𝐺)) = (𝐴 ∘f + 𝐵) ∧ (deg‘(𝐹 ∘f + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)))
Theorem	coemullem 26171*	Lemma for coemul 26173 and dgrmul 26192. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    &   ⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐹 ∘f · 𝐺)) = (𝑛 ∈ ℕ0 ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘)))) ∧ (deg‘(𝐹 ∘f · 𝐺)) ≤ (𝑀 + 𝑁)))
Theorem	coeadd 26172	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 26173*	A coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0) → ((coeff‘(𝐹 ∘f · 𝐺))‘𝑁) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝐵‘(𝑁 − 𝑘))))
Theorem	coe11 26174	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 26175	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 26176	The coefficient function is linear under scalar multiplication. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘((ℂ × {𝐴}) ∘f · 𝐹)) = ((ℕ0 × {𝐴}) ∘f · (coeff‘𝐹)))
Theorem	coe0 26177	The coefficients of the zero polynomial are zero. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (coeff‘0𝑝) = (ℕ0 × {0})
Theorem	coesub 26178	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 26179*	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 26180*	The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((coeff‘𝐹)‘𝑀) = if(𝑀 = 𝑁, 𝐴, 0))
Theorem	dgr1term 26181*	The degree of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℕ0) → (deg‘𝐹) = 𝑁)
Theorem	plycn 26182	A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 11108. (Revised by GG, 16-Mar-2025.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	plycnOLD 26183	Obsolete version of plycn 26182 as of 10-Apr-2025. (Contributed by Mario Carneiro, 23-Jul-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	dgr0 26184	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 26154, dgreq0 26187 and coeid 26159 without having to special-case zero, although plydivalg 26223 is a little more complicated as a result. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (deg‘0𝑝) = 0
Theorem	coeidp 26185	The coefficients of the identity function. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ (𝐴 ∈ ℕ0 → ((coeff‘Xp)‘𝐴) = if(𝐴 = 1, 1, 0))
Theorem	dgrid 26186	The degree of the identity function. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ (deg‘Xp) = 1
Theorem	dgreq0 26187	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 26188	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 26189	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(𝑀 ≤ 𝑁, 𝑁, 𝑀))
Theorem	dgradd2 26190	The degree of a sum of polynomials of unequal degrees is the degree of the larger polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) = 𝑁)
Theorem	dgrmul2 26191	The degree of a product of polynomials is at most the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘f · 𝐺)) ≤ (𝑀 + 𝑁))
Theorem	dgrmul 26192	The degree of a product of nonzero polynomials is the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) → (deg‘(𝐹 ∘f · 𝐺)) = (𝑀 + 𝑁))
Theorem	dgrmulc 26193	Scalar multiplication by a nonzero constant does not change the degree of a function. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘((ℂ × {𝐴}) ∘f · 𝐹)) = (deg‘𝐹))
Theorem	dgrsub 26194	The degree of a difference of polynomials is at most the maximum of the degrees. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘f − 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))
Theorem	dgrcolem1 26195*	The degree of a composition of a monomial with a polynomial. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ 𝑁 = (deg‘𝐺)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    ⇒   ⊢ (𝜑 → (deg‘(𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀))) = (𝑀 · 𝑁))
Theorem	dgrcolem2 26196*	Lemma for dgrco 26197. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 = (𝐷 + 1))    &   ⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))    ⇒   ⊢ (𝜑 → (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁))
Theorem	dgrco 26197	The degree of a composition of two polynomials is the product of the degrees. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    ⇒   ⊢ (𝜑 → (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁))
Theorem	plycjlem 26198*	Lemma for plycj 26199 and coecj 26200. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   ⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘))))
Theorem	plycj 26199*	The double conjugation of a polynomial is a polynomial. (The single conjugation is not because our definition of polynomial includes only holomorphic functions, i.e. no dependence on (∗‘𝑧) independently of 𝑧.) (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∗‘𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))
Theorem	coecj 26200	Double conjugation of a polynomial causes the coefficients to be conjugated. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   ⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐺) = (∗ ∘ 𝐴))